A2:
F is_naturally_transformable_to F2
by A1, Th8;

A3: ( ( 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) ) & ( 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 A1, Def7;

( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1;

then 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, Lm2;

then t2 `*` t1 is natural_transformation of F,F2 by A2, Def7;

hence ex b_{1} being natural_transformation of F,F2 st b_{1} = t2 `*` t1
; :: thesis: verum

A3: ( ( 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) ) & ( 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 A1, Def7;

( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1;

then 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, Lm2;

then t2 `*` t1 is natural_transformation of F,F2 by A2, Def7;

hence ex b