'Environmental' problems

Борис Шминке <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
Dear all,
I'm only a stupid newbie and it was hard for me even to start using
this forum, but I have a question. Yes, unfortunately to all
experienced users of Mizar System, the question is about environment
section of an article. I've read the advises to copy it from some
article on the relevant theme, but I still want to understand how it
works.
So, what I have:
environ
  vocabularies ARYTM_3, NAT_1;
  notations    ARYTM_3, NAT_1;
  constructors ARYTM_3, NAT_1;
  registrations NAT_1;
begin
  reserve x, y for Nat;
  theorem x + y = x + y
::>         *103    *103
  proof
  end;
::> 103: Unknown functor

I've added 'registrations NAT_1' line because there is a cluster:
registration
  let n,k be Nat;
  cluster n + k -> natural;
end;
in NAT_1. So I expected, that it would be enough, but it wasn't.
Could you explain me, why the functor '+' is still unknown? How to
correct the situation and why it will be correct?
Regards,
Boris Schminke.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.