A2:
G1 is_transformable_to G2
by A1, NATTRA_1:def 7;
t * F is natural_transformation of G1 * F,G2 * F
proof
thus
G1 * F is_naturally_transformable_to G2 * F
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 ((t * F) . b2) * ((G1 * F) . b3) = ((G2 * F) . b3) * ((t * F) . b1) )
then A3:
G1 * F is_transformable_to G2 * F
by NATTRA_1:def 7;
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, NATTRA_1:def 2;
A5:
Hom (
((G1 * F) . a),
((G2 * F) . a))
<> {}
by A3, NATTRA_1:def 2;
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, NATTRA_1:def 2;
A11:
Hom (
(G1 . (F . b)),
(G2 . (F . b)))
<> {}
by A2, NATTRA_1:def 2;
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 10
.=
((t * F) . b) * (G1 . (F . f))
by A6, NATTRA_1:11
.=
(t . (F . b)) * (G1 . (F . f))
by A2, Th25
.=
(t . (F . b)) * (G1 . (F . f))
by A11, A9, CAT_1:def 10
.=
(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 10
.=
(G2 . (F . f)) * ((t * F) . a)
by A2, Th25
.=
((G2 * F) . f) * ((t * F) . a)
by A6, NATTRA_1:11
.=
((G2 * F) . f) * ((t * F) . a)
by A7, A5, CAT_1:def 10
;
verum
end;
hence
t * F is natural_transformation of G1 * F,G2 * F
; verum