reconsider Gt = G * t as Function of the carrier of A, the carrier' of C ;
Gt is transformation of G * F1,G * F2

proof

thus G * F1 is_transformable_to G * F2 by A1, Th3; :: according to NATTRA_1:def 3 :: thesis: for b₁ being M3( the carrier of A) holds Gt . b₁ is Morphism of (G * F1) . b₁,(G * F2) . b₁
let a be Object of A; :: thesis: Gt . a is Morphism of (G * F1) . a,(G * F2) . a
A2: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76;
t . a in Hom ((F1 . a),(F2 . a)) by A1, Th2;
then A3: G . (t . a) in Hom (((G * F1) . a),((G * F2) . a)) by A2, CAT_1:81;
Gt . a = G . (t . a) by FUNCT_2:15
.= G . (t . a) by A1, NATTRA_1:def 5 ;
hence Gt . a is Morphism of (G * F1) . a,(G * F2) . a by A3, CAT_1:def 5; :: thesis: verum

end;

hence G * t is transformation of G * F1,G * F2 ; :: thesis: verum