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