defpred S₁[ set , set ] means ex o being object of A st
( $1 = o & $2 = G . (t ! o) );
set I = the carrier of A;
A2: for i being set st i in the carrier of A holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in the carrier of A implies ex j being set st S₁[i,j] )
assume i in the carrier of A ; :: thesis: ex j being set st S₁[i,j]
then reconsider o = i as object of A ;
take G . (t ! o) ; :: thesis: S₁[i,G . (t ! o)]
thus S₁[i,G . (t ! o)] ; :: thesis: verum

end;

consider IT being ManySortedSet of the carrier of A such that
A3: for o being set st o in the carrier of A holds
S₁[o,IT . o] from PBOOLE:sch 3(A2);
IT is transformation of G * F1,G * F2

proof

thus G * F1 is_transformable_to G * F2 by A1, Th10; :: according to FUNCTOR2:def 2 :: thesis: for b₁ being M2( the carrier of A) holds IT . b₁ is M2(<^((G * F1) . b₁),((G * F2) . b₁)^>)
let o be object of A; :: thesis: IT . o is M2(<^((G * F1) . o),((G * F2) . o)^>)
( S₁[o,IT . o] & G . (F1 . o) = (G * F1) . o ) by A3, FUNCTOR0:33;
hence IT . o is M2(<^((G * F1) . o),((G * F2) . o)^>) by FUNCTOR0:33; :: thesis: verum

end;

then reconsider IT = IT as transformation of G * F1,G * F2 ;
take IT ; :: thesis: for o being object of A holds IT . o = G . (t ! o)
let o be object of A; :: thesis: IT . o = G . (t ! o)
S₁[o,IT . o] by A3;
hence IT . o = G . (t ! o) ; :: thesis: verum