let A, B be non empty transitive with_units AltCatStr ; :: 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 A1: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) ; :: thesis: F is_transformable_to F2
let a be Object of A; :: according to FUNCTOR2:def 1 :: thesis: <^(F . a),(F2 . a)^> <> {}
( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1;
hence <^(F . a),(F2 . a)^> <> {} by ALTCAT_1:def 2; :: thesis: verum