let A, B, C be Category; :: thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
<:F1,F2:> is_transformable_to <:G1,G2:>
let F1, G1 be Functor of A,B; :: thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
<:F1,F2:> is_transformable_to <:G1,G2:>
let F2, G2 be Functor of A,C; :: thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies <:F1,F2:> is_transformable_to <:G1,G2:> )
assume A1: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) ; :: thesis: <:F1,F2:> is_transformable_to <:G1,G2:>
let a be Object of A; :: according to NATTRA_1:def 2 :: thesis: not Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) = {}
thus not Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) = {} by A1, Lm3; :: thesis: verum