A2:
G1 is_transformable_to G2
by A1, NATTRA_1:def 7;
t * F is natural_transformation of G1 * F,G2 * F
proof
thus
G1 * F is_naturally_transformable_to G2 * F
by A1, Th27;
NATTRA_1:def 8 for b1, b2 being M2(the carrier of A) holds
( Hom b1,b2 = {} or for b3 being Morphism of b1,b2 holds ((t * F) . b2) * ((G1 * F) . b3) = ((G2 * F) . b3) * ((t * F) . b1) )
then A3:
G1 * F is_transformable_to G2 * F
by NATTRA_1:def 7;
let a,
b be
Object of
A;
( Hom a,b = {} or for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) . b1) = ((G2 * F) . b1) * ((t * F) . a) )
A4:
Hom ((G1 * F) . b),
((G2 * F) . b) <> {}
by A3, NATTRA_1:def 2;
A5:
Hom ((G1 * F) . a),
((G2 * F) . a) <> {}
by A3, NATTRA_1:def 2;
assume A6:
Hom a,
b <> {}
;
for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) . b1) = ((G2 * F) . b1) * ((t * F) . a)
then A7:
Hom ((G2 * F) . a),
((G2 * F) . b) <> {}
by CAT_1:126;
let f be
Morphism of
a,
b;
((t * F) . b) * ((G1 * F) . f) = ((G2 * F) . f) * ((t * F) . a)
A8:
Hom (F . a),
(F . b) <> {}
by A6, CAT_1:126;
then A9:
Hom (G1 . (F . a)),
(G1 . (F . b)) <> {}
by CAT_1:126;
A10:
Hom (G1 . (F . a)),
(G2 . (F . a)) <> {}
by A2, NATTRA_1:def 2;
A11:
Hom (G1 . (F . b)),
(G2 . (F . b)) <> {}
by A2, NATTRA_1:def 2;
A12:
Hom (G2 . (F . a)),
(G2 . (F . b)) <> {}
by A8, CAT_1:126;
Hom ((G1 * F) . a),
((G1 * F) . b) <> {}
by A6, CAT_1:126;
hence ((t * F) . b) * ((G1 * F) . f) =
((t * F) . b) * ((G1 * F) . f)
by A4, CAT_1:def 13
.=
((t * F) . b) * (G1 . (F . f))
by A6, NATTRA_1:11
.=
(t . (F . b)) * (G1 . (F . f))
by A2, Th25
.=
(t . (F . b)) * (G1 . (F . f))
by A11, A9, CAT_1:def 13
.=
(G2 . (F . f)) * (t . (F . a))
by A1, A8, NATTRA_1:def 8
.=
(G2 . (F . f)) * (t . (F . a))
by A12, A10, CAT_1:def 13
.=
(G2 . (F . f)) * ((t * F) . a)
by A2, Th25
.=
((G2 * F) . f) * ((t * F) . a)
by A6, NATTRA_1:11
.=
((G2 * F) . f) * ((t * F) . a)
by A7, A5, CAT_1:def 13
;
verum
end;
hence
t * F is natural_transformation of G1 * F,G2 * F
; verum