defpred S_{1}[ Object of A, object ] means $2 in <^(F1 . $1),(F2 . $1)^>;

A2: for a being Element of A ex j being object st S_{1}[a,j]

A3: for a being Element of A holds S_{1}[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

A2: for a being Element of A ex j being object st S

proof

consider t being ManySortedSet of the carrier of A such that
let a be Element of A; :: thesis: ex j being object st S_{1}[a,j]

<^(F1 . a),(F2 . a)^> <> {} by A1;

then ex j being object st j in <^(F1 . a),(F2 . a)^> by XBOOLE_0:def 1;

hence ex j being object st S_{1}[a,j]
; :: thesis: verum

end;<^(F1 . a),(F2 . a)^> <> {} by A1;

then ex j being object st j in <^(F1 . a),(F2 . a)^> by XBOOLE_0:def 1;

hence ex j being object st S

A3: for a being Element of A holds S

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