A3:
( F is_transformable_to F1 & F1 is_transformable_to F2 )
by A1, A2, Def6;
A4:
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a)
by A1, Def7;
A5:
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a)
by A2, Def7;
t2 `*` t1 is natural_transformation of F,F2
proof
thus
F is_naturally_transformable_to F2
by A1, A2, Th10;
:: according to FUNCTOR2:def 7 :: thesis: for a, b being object of A st <^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
<^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
ex b1 being natural_transformation of F,F2 st b1 = t2 `*` t1
; :: thesis: verum