defpred S₁[ set , set ] means ex o being object of A st
( $1 = o & $2 = s ! (F . 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 s ! (F . o) ; :: thesis: S₁[i,s ! (F . o)]
thus S₁[i,s ! (F . 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 G1 * F,G2 * F

proof

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

end;

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