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, Th8;
NATTRA_1:def 3 for b1 being M2(the carrier of A) holds Gt . b1 is Morphism of (G * F1) . b1,(G * F2) . b1
let a be
Object of
A;
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:113;
t . a in Hom (F1 . a),
(F2 . a)
by A1, Th7;
then A3:
G . (t . a) in Hom ((G * F1) . a),
((G * F2) . a)
by A2, CAT_1:123;
Gt . a =
G . (t . a)
by FUNCT_2:21
.=
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 7;
verum
end;
hence
G * t is transformation of G * F1,G * F2
; verum