let A, B be Category; for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
F1 ~= F3
let F1, F2, F3 be Functor of A,B; ( F1 ~= F2 & F2 ~= F3 implies F1 ~= F3 )
assume A1:
F1 is_naturally_transformable_to F2
; NATTRA_1:def 11 ( for t being natural_transformation of F1,F2 holds not t is invertible or not F2 ~= F3 or F1 ~= F3 )
given t being natural_transformation of F1,F2 such that A2:
t is invertible
; ( not F2 ~= F3 or F1 ~= F3 )
assume A3:
F2 is_naturally_transformable_to F3
; NATTRA_1:def 11 ( for t being natural_transformation of F2,F3 holds not t is invertible or F1 ~= F3 )
given t9 being natural_transformation of F2,F3 such that A4:
t9 is invertible
; F1 ~= F3
thus
F1 is_naturally_transformable_to F3
by A1, A3, Th19; NATTRA_1:def 11 ex t being natural_transformation of F1,F3 st t is invertible
take
t9 `*` t
; t9 `*` t is invertible
let a be Object of A; NATTRA_1:def 10 (t9 `*` t) . a is invertible
A5:
t9 . a is invertible
by A4;
A6:
t . a is invertible
by A2;
(t9 `*` t) . a = (t9 . a) * (t . a)
by A1, A3, Th21;
hence
(t9 `*` t) . a is invertible
by A5, A6, CAT_1:45; verum