deffunc H₁( set ) -> object = [$1,F₂($1)];
defpred S₁[ set , set ] means P₁[$1];

per cases ( not F₁() is empty or F₁() is empty ) ;

suppose not F₁() is empty ; :: thesis: { [o,F₂(o)] where o is Element of F₁() : P₁[o] } is Function

then reconsider XX = F₁() as non empty set ;
{ [o,F₂(o)] where o is Element of XX : P₁[o] } is Function from ALTCAT_2:sch 1();
hence { [o,F₂(o)] where o is Element of F₁() : P₁[o] } is Function ; :: thesis: verum

end;

suppose F₁() is empty ; :: thesis: { [o,F₂(o)] where o is Element of F₁() : P₁[o] } is Function

then reconsider XX = F₁() as trivial set ;
{ H₁(o) where o is Element of XX : S₁[o,XX] } c= {H₁( the Element of XX)} from FOMODEL0:sch 2();
hence { [o,F₂(o)] where o is Element of F₁() : P₁[o] } is Function ; :: thesis: verum

end;

end;