defpred S1[ 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 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 G . (t ! o) ; :: thesis: S1[i,G . (t ! o)]
thus S1[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
S1[o,IT . o] from IT is transformation of G * F1,G * F2
proof
thus G * F1 is_transformable_to G * F2 by ; :: according to FUNCTOR2:def 2 :: thesis: for b1 being M3( the carrier of A) holds IT . b1 is M3(<^((G * F1) . b1),((G * F2) . b1)^>)
let o be Object of A; :: thesis: IT . o is M3(<^((G * F1) . o),((G * F2) . o)^>)
( S1[o,IT . o] & G . (F1 . o) = (G * F1) . o ) by ;
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)
S1[o,IT . o] by A3;
hence IT . o = G . (t ! o) ; :: thesis: verum