[mizar] "mode Element of ...", some questions...

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Dear All,

I would like to ask a question but before that please let me present the following Mizar fragment:


definition
  func setA -> set equals
    {k where k is Element of NAT: k < 15};
  correctness;
end;

definition
  let e be Element of setA;
  func f(e) -> Element of setA means
    ...
end;

f(1) = ...; 
::>*103  (Unknown Functor)


1 is Element of setA; 
::>                         *4 (This inference is not accepted)


My questions are 
(1) how to make Mizar accept "1 is Element of setA"? I checked the MML for "mode Element of ..." examples and could not find anything that could help me. 
(2) This relates to the Question (1). How can I make sure that 1 is known to be an Element of setA so that 103 error does not occur?


Thank you all and I always appreciate the group's help.
Regards,

Adem Ozyavas
Texas Tech University