A2:
F1 is_transformable_to F2
by A1, 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 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 ((G * t) . b2) * ((G * F1) . b3) = ((G * F2) . b3) * ((G * t) . b1) )
then A3:
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 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, NATTRA_1:def 2;
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, NATTRA_1:def 2;
then A9:
Hom (
(G . (F1 . b)),
(G . (F2 . b)))
<> {}
by CAT_1:84;
A10:
Hom (
(F1 . a),
(F2 . a))
<> {}
by A2, NATTRA_1:def 2;
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, NATTRA_1:def 2;
hence ((G * t) . b) * ((G * F1) . f) =
((G * t) . b) * ((G * F1) . f)
by A5, CAT_1:def 10
.=
((G * t) . b) * (G . (F1 . f))
by A4, NATTRA_1:11
.=
(G . (t . b)) * (G . (F1 . f))
by A2, Th26
.=
(G . (t . b)) * (G . (F1 . f))
by A9, A15, CAT_1:def 10
.=
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 10
.=
(G . (F2 . f)) * ((G * t) . a)
by A2, Th26
.=
((G * F2) . f) * ((G * t) . a)
by A4, NATTRA_1:11
.=
((G * F2) . f) * ((G * t) . a)
by A7, A6, CAT_1:def 10
;
verum
end;
hence
G * t is natural_transformation of G * F1,G * F2
; verum