A2:
G1 is_transformable_to G2
by A1;
t * F is natural_transformation of G1 * F,G2 * F
proof
thus
G1 * F is_naturally_transformable_to G2 * F
by A1, Th20;
NATTRA_1:def 8 for b1, b2 being M3( 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
;
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;
A5:
Hom (
((G1 * F) . a),
((G2 * F) . a))
<> {}
by A3;
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:84;
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:84;
then A9:
Hom (
(G1 . (F . a)),
(G1 . (F . b)))
<> {}
by CAT_1:84;
A10:
Hom (
(G1 . (F . a)),
(G2 . (F . a)))
<> {}
by A2;
A11:
Hom (
(G1 . (F . b)),
(G2 . (F . b)))
<> {}
by A2;
A12:
Hom (
(G2 . (F . a)),
(G2 . (F . b)))
<> {}
by A8, CAT_1:84;
Hom (
((G1 * F) . a),
((G1 * F) . b))
<> {}
by A6, CAT_1:84;
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, Th18
.=
(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, Th18
.=
((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