let A, B be Category; :: thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2
let F, F1, F2 be Functor of A,B; :: thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2 )
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 ; :: thesis: F is_transformable_to F2
let a be Object of A; :: according to NATTRA_1:def 2 :: thesis: Hom (F . a),(F2 . a) <> {}
A3: Hom (F1 . a),(F2 . a) <> {} by A2, Def2;
Hom (F . a),(F1 . a) <> {} by A1, Def2;
hence Hom (F . a),(F2 . a) <> {} by A3, CAT_1:52; :: thesis: verum