A2:
F1 is_transformable_to F2
by A1;
G * t is natural_transformation of G * F1,G * F2
proof
thus
G * F1 is_naturally_transformable_to G * F2
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 ((G * t) . b2) * ((G * F1) /. b3) = ((G * F2) /. b3) * ((G * t) . b1) )
then A3:
G * F1 is_transformable_to G * F2
;
let a,
b be
Object of
A;
( Hom (a,b) = {} or for b1 being Morphism of a,b holds ((G * t) . b) * ((G * F1) /. b1) = ((G * F2) /. b1) * ((G * t) . a) )
assume A4:
Hom (
a,
b)
<> {}
;
for b1 being Morphism of a,b holds ((G * t) . b) * ((G * F1) /. b1) = ((G * F2) /. b1) * ((G * t) . a)
A5:
Hom (
((G * F1) . a),
((G * F1) . b))
<> {}
by A4, CAT_1:84;
A6:
Hom (
((G * F2) . a),
((G * F2) . b))
<> {}
by A4, CAT_1:84;
A7:
Hom (
((G * F1) . a),
((G * F2) . a))
<> {}
by A3;
let f be
Morphism of
a,
b;
((G * t) . b) * ((G * F1) /. f) = ((G * F2) /. f) * ((G * t) . a)
A8:
Hom (
(F1 . b),
(F2 . b))
<> {}
by A2;
then A9:
Hom (
(G . (F1 . b)),
(G . (F2 . b)))
<> {}
by CAT_1:84;
A10:
Hom (
(F1 . a),
(F2 . a))
<> {}
by A2;
then A11:
Hom (
(G . (F1 . a)),
(G . (F2 . a)))
<> {}
by CAT_1:84;
A12:
Hom (
(F2 . a),
(F2 . b))
<> {}
by A4, CAT_1:84;
then A13:
Hom (
(G . (F2 . a)),
(G . (F2 . b)))
<> {}
by CAT_1:84;
A14:
Hom (
(F1 . a),
(F1 . b))
<> {}
by A4, CAT_1:84;
then A15:
Hom (
(G . (F1 . a)),
(G . (F1 . b)))
<> {}
by CAT_1:84;
Hom (
((G * F1) . b),
((G * F2) . b))
<> {}
by A3;
hence ((G * t) . b) * ((G * F1) /. f) =
((G * t) . b) (*) ((G * F1) /. f)
by A5, CAT_1:def 13
.=
((G * t) . b) (*) (G /. (F1 /. f))
by A4, NATTRA_1:11
.=
(G /. (t . b)) (*) (G /. (F1 /. f))
by A2, Th19
.=
(G /. (t . b)) * (G /. (F1 /. f))
by A9, A15, CAT_1:def 13
.=
G /. ((t . b) * (F1 /. f))
by A8, A14, NATTRA_1:13
.=
G /. ((F2 /. f) * (t . a))
by A1, A4, NATTRA_1:def 8
.=
(G /. (F2 /. f)) * (G /. (t . a))
by A10, A12, NATTRA_1:13
.=
(G /. (F2 /. f)) (*) (G /. (t . a))
by A13, A11, CAT_1:def 13
.=
(G /. (F2 /. f)) (*) ((G * t) . a)
by A2, Th19
.=
((G * F2) /. f) (*) ((G * t) . a)
by A4, NATTRA_1:11
.=
((G * F2) /. f) * ((G * t) . a)
by A7, A6, CAT_1:def 13
;
verum
end;
hence
G * t is natural_transformation of G * F1,G * F2
; verum