let A, B, C be Category; :: thesis: for F being Functor of [:A,B:],C
for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
let F be Functor of [:A,B:],C; :: thesis: for g being Morphism of A holds F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
let g be Morphism of A; :: thesis: F ?- (dom g) is_naturally_transformable_to F ?- (cod g)
Hom ((dom g),(cod g)) <> {} by CAT_1:2;
hence F ?- (dom g) is_naturally_transformable_to F ?- (cod g) by Th13; :: thesis: verum