[mizar] Question on Mizar grammar

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi All,

The article funct_2.miz contains the following fragment (lines 933 - 937):

-------------------------------
registration let X;
  let f,g be quasi_total PartFunc of X,X;
  cluster g*f -> quasi_total PartFunc of X,X;
  coherence proof X <> {} or X = {}; hence thesis by Th19; end;
end;
-------------------------------

but the current production rule for functorial registration doesn't allow type 
expression:

Functorial-Registration =
	"cluster" Term-Expression "->" Adjective-Cluster ";" Correctness-Conditions .

It seems this rule must be like the following (though I am not sure about it).

Functorial-Registration =
	"cluster" Term-Expression "->" Adjective-Cluster [ Type-Expression] ";" 
Correctness-Conditions .

Can anyone confirm it?

Michael Nedzelsky