let B, A be Category; :: thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for a being Object of A holds Hom (F1 . a),(F2 . a) <> {}
let F1, F2 be Functor of A,B; :: thesis: ( F1 is_naturally_transformable_to F2 implies for a being Object of A holds Hom (F1 . a),(F2 . a) <> {} )
assume F1 is_naturally_transformable_to F2 ; :: thesis: for a being Object of A holds Hom (F1 . a),(F2 . a) <> {}
then A1: F1 is_transformable_to F2 by NATTRA_1:def 7;
let a be Object of A; :: thesis: Hom (F1 . a),(F2 . a) <> {}
thus Hom (F1 . a),(F2 . a) <> {} by A1, NATTRA_1:def 2; :: thesis: verum