deffunc H1( set ) -> object = [$1,F2($1)];
defpred S1[ set , set ] means P1[$1];
per cases ( not F1() is empty or F1() is empty ) ;
suppose not F1() is empty ; :: thesis: { [o,F2(o)] where o is Element of F1() : P1[o] } is Function
then reconsider XX = F1() as non empty set ;
{ [o,F2(o)] where o is Element of XX : P1[o] } is Function from ALTCAT_2:sch 1();
hence { [o,F2(o)] where o is Element of F1() : P1[o] } is Function ; :: thesis: verum
end;
suppose F1() is empty ; :: thesis: { [o,F2(o)] where o is Element of F1() : P1[o] } is Function
then reconsider XX = F1() as trivial set ;
{ H1(o) where o is Element of XX : S1[o,XX] } c= {H1( the Element of XX)} from FOMODEL0:sch 2();
hence { [o,F2(o)] where o is Element of F1() : P1[o] } is Function ; :: thesis: verum
end;
end;