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

proof

let i be object ; :: thesis: ( i in the carrier of A implies ex j being object st S₁[i,j] )
assume i in the carrier of A ; :: thesis: ex j being object 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 object 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 M3( the carrier of A) holds IT . b₁ is M3(<^((G * F1) . b₁),((G * F2) . b₁)^>)
let o be Object of A; :: thesis: IT . o is M3(<^((G * F1) . o),((G * F2) . o)^>)
( S₁[o,IT . o] & G . (F1 . o) = (G * F1) . o ) by A3, FUNCTOR0:33;
hence IT . o is M3(<^((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