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

proof

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

end;

consider t being ManySortedSet of the carrier of A such that
A3: for a being Element of A holds S₁[a,t . a] from PBOOLE:sch 6(A2);
take t ; :: thesis: for a being object of A holds t . a is Morphism of (F1 . a),(F2 . a)
thus for a being object of A holds t . a is Morphism of (F1 . a),(F2 . a) by A3; :: thesis: verum