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 b₁ being M3( the carrier of A) holds tF . b₁ is Morphism of (G1 * F) . b₁,(G2 * F) . b₁
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