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:126;
A6:
Hom ((G * F2) . a),
((G * F2) . b) <> {}
by A4, CAT_1:126;
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:126;
A10:
Hom (F1 . a),
(F2 . a) <> {}
by A2, NATTRA_1:def 2;
then A11:
Hom (G . (F1 . a)),
(G . (F2 . a)) <> {}
by CAT_1:126;
A12:
Hom (F2 . a),
(F2 . b) <> {}
by A4, CAT_1:126;
then A13:
Hom (G . (F2 . a)),
(G . (F2 . b)) <> {}
by CAT_1:126;
A14:
Hom (F1 . a),
(F1 . b) <> {}
by A4, CAT_1:126;
then A15:
Hom (G . (F1 . a)),
(G . (F1 . b)) <> {}
by CAT_1:126;
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 13
.=
((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 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, Th26
.=
((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