A3:
( F is_transformable_to F1 & F1 is_transformable_to F2 )
by A1, A2, Def7;
A4:
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t1 . b) * (F . f) = (F1 . f) * (t1 . a)
by A1, Def8;
A5:
for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds (t2 . b) * (F1 . f) = (F2 . f) * (t2 . a)
by A2, Def8;
t2 `*` t1 is natural_transformation of F,F2
proof
thus
F is_naturally_transformable_to F2
by A1, A2, Th25;
:: according to NATTRA_1:def 8 :: thesis: for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
thus
for
a,
b being
Object of
A st
Hom a,
b <> {} holds
for
f being
Morphism of
a,
b holds
((t2 `*` t1) . b) * (F . f) = (F2 . f) * ((t2 `*` t1) . a)
by A3, A4, A5, Lm2;
:: thesis: verum
end;
hence
t2 `*` t1 is natural_transformation of F,F2
; :: thesis: verum