defpred S₁[ Object of A, object ] means $2 = (t2 ! $1) * (t1 ! $1);
A2: for a being Element of A ex j being object st S₁[a,j] ;
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);
A4: F is_transformable_to F2 by A1, Th2;
for a being Object of A holds t . a is Morphism of (F . a),(F2 . a)

proof

let o be Element of A; :: thesis: t . o is Morphism of (F . o),(F2 . o)
S₁[o,t . o] by A3;
hence t . o is Morphism of (F . o),(F2 . o) ; :: thesis: verum

end;

then reconsider t9 = t as transformation of F,F2 by A4, Def2;
take t9 ; :: thesis: for a being Object of A holds t9 ! a = (t2 ! a) * (t1 ! a)
let a be Element of A; :: thesis: t9 ! a = (t2 ! a) * (t1 ! a)
S₁[a,t . a] by A3;
hence t9 ! a = (t2 ! a) * (t1 ! a) by A4, Def4; :: thesis: verum