defpred S1[ object , object ] means ex o being Object of A st
( $1 = o & $2 = s ! (F . 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 S1[i,j]
proof
let i be object ; :: thesis: ( i in the carrier of A implies ex j being object st S1[i,j] )
assume i in the carrier of A ; :: thesis: ex j being object st S1[i,j]
then reconsider o = i as Object of A ;
take s ! (F . o) ; :: thesis: S1[i,s ! (F . o)]
thus S1[i,s ! (F . 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
S1[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 b1 being M3( the carrier of A) holds IT . b1 is M3(<^((G1 * F) . b1),((G2 * F) . b1)^>)
let o be Object of A; :: thesis: IT . o is M3(<^((G1 * F) . o),((G2 * F) . o)^>)
( S1[o,IT . o] & G1 . (F . o) = (G1 * F) . o ) by A3, FUNCTOR0:33;
hence IT . o is M3(<^((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)
S1[o,IT . o] by A3;
hence IT . o = s ! (F . o) ; :: thesis: verum