defpred S₁[ set , set ] means ex o being object of st
( $1 = o & $2 in <^(F1 . o),(F2 . o)^> );
A2: for a being Element of ex j being set st S₁[a,j]

proof

let a be Element of ; :: thesis: ex j being set st S₁[a,j]
reconsider o = a as object of ;
<^(F1 . o),(F2 . o)^> <> {} by A1, Def1;
then ex j being set st j in <^(F1 . o),(F2 . o)^> by XBOOLE_0:def 1;
hence ex j being set st S₁[a,j] ; :: thesis: verum

end;

consider t being ManySortedSet of the carrier of A such that
A3: for a being Element of holds S₁[a,t . a] from PBOOLE:sch 6(A2);
take t ; :: thesis: for a being object of holds t . a is Morphism of ,
let a be object of ; :: thesis: t . a is Morphism of ,
ex o being object of st
( a = o & t . a in <^(F1 . o),(F2 . o)^> ) by A3;
hence t . a is Morphism of , ; :: thesis: verum