A1:
G1 is_transformable_to G2
by B1, 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 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 ((t * F) . b2) * ((G1 * F) /. b3) = ((G2 * F) /. b3) * ((t * F) . b1) )
then A2:
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) )
A3:
Hom (
((G1 * F) . b),
((G2 * F) . b))
<> {}
by A2, NATTRA_1:def 2;
A4:
Hom (
((G1 * F) . a),
((G2 * F) . a))
<> {}
by A2, NATTRA_1:def 2;
assume A5:
Hom (
a,
b)
<> {}
;
for b1 being Morphism of a,b holds ((t * F) . b) * ((G1 * F) /. b1) = ((G2 * F) /. b1) * ((t * F) . a)
then A6:
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)
A7:
Hom (
(F . a),
(F . b))
<> {}
by A5, CAT_1:84;
then A8:
Hom (
(G1 . (F . a)),
(G1 . (F . b)))
<> {}
by CAT_1:84;
A9:
Hom (
(G1 . (F . a)),
(G2 . (F . a)))
<> {}
by A1, NATTRA_1:def 2;
A10:
Hom (
(G1 . (F . b)),
(G2 . (F . b)))
<> {}
by A1, NATTRA_1:def 2;
A11:
Hom (
(G2 . (F . a)),
(G2 . (F . b)))
<> {}
by A7, CAT_1:84;
Hom (
((G1 * F) . a),
((G1 * F) . b))
<> {}
by A5, CAT_1:84;
hence ((t * F) . b) * ((G1 * F) /. f) =
((t * F) . b) (*) ((G1 * F) /. f)
by A3, CAT_1:def 13
.=
((t * F) . b) (*) (G1 /. (F /. f))
by A5, NATTRA_1:11
.=
(t . (F . b)) (*) (G1 /. (F /. f))
by A1, Th20
.=
(t . (F . b)) * (G1 /. (F /. f))
by A10, A8, CAT_1:def 13
.=
(G2 /. (F /. f)) * (t . (F . a))
by B1, A7, NATTRA_1:def 8
.=
(G2 /. (F /. f)) (*) (t . (F . a))
by A11, A9, CAT_1:def 13
.=
(G2 /. (F /. f)) (*) ((t * F) . a)
by A1, Th20
.=
((G2 * F) /. f) (*) ((t * F) . a)
by A5, NATTRA_1:11
.=
((G2 * F) /. f) * ((t * F) . a)
by A6, A4, CAT_1:def 13
;
verum
end;
hence
t * F is natural_transformation of G1 * F,G2 * F
; verum