reconsider tF = t * (Obj F) as Function of the carrier of A, the carrier' of C ;
tF is transformation of G1 * F,G2 * F
proof
thus G1 * F is_transformable_to G2 * F by A1, Th3; :: according to NATTRA_1:def 3 :: thesis: for b1 being M3( the carrier of A) holds tF . b1 is Morphism of (G1 * F) . b1,(G2 * F) . b1
let a be Object of A; :: thesis: tF . a is Morphism of (G1 * F) . a,(G2 * F) . a
A2: G1 . (F . a) = (G1 * F) . a by CAT_1:76;
tF . a = t . ((Obj F) . a) by FUNCT_2:15
.= t . (F . a) by A1, NATTRA_1:def 5 ;
hence tF . a is Morphism of (G1 * F) . a,(G2 * F) . a by A2, CAT_1:76; :: thesis: verum
end;
hence t * (Obj F) is transformation of G1 * F,G2 * F ; :: thesis: verum