let A, B be Category; for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let F1, F2 be Functor of A,B; ( F1 is_transformable_to F2 implies for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a)) )
assume A1:
F1 is_transformable_to F2
; for t being transformation of F1,F2
for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let t be transformation of F1,F2; for a being Object of A holds t . a in Hom ((F1 . a),(F2 . a))
let a be Object of A; t . a in Hom ((F1 . a),(F2 . a))
Hom ((F1 . a),(F2 . a)) <> {}
by A1;
hence
t . a in Hom ((F1 . a),(F2 . a))
by CAT_1:def 5; verum