defpred S₁[ set , set ] means ex o being object of A st
( $1 = o & $2 = (t2 ! o) * (t1 ! o) );
A3: 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 ;
consider j being set such that
A4: j = (t2 ! o) * (t1 ! o) ;
thus ex j being set st S₁[a,j] by A4; :: thesis: verum

end;

consider t being ManySortedSet of such that
A5: for a being Element of A holds S₁[a,t . a] from PBOOLE:sch 6(A3);
A6: F is_transformable_to F2 by A1, A2, Th4;
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)
consider a being object of A such that
A7: ( o = a & t . o = (t2 ! a) * (t1 ! a) ) by A5;
thus t . o is Morphism of (F . o),(F2 . o) by A7; :: thesis: verum

end;

then reconsider t' = t as transformation of F,F2 by A6, Def2;
take t' ; :: thesis: for a being object of A holds t' ! a = (t2 ! a) * (t1 ! a)
let a be Element of A; :: thesis: t' ! a = (t2 ! a) * (t1 ! a)
consider o being object of A such that
A8: ( a = o & t . a = (t2 ! o) * (t1 ! o) ) by A5;
thus t' ! a = (t2 ! a) * (t1 ! a) by A6, A8, Def4; :: thesis: verum