let o, m be set ; :: thesis: for a, b being Object of
for f being Morphism of holds f is Morphism of a,b
let a, b be Object of ; :: thesis: for f being Morphism of holds f is Morphism of a,b
let f be Morphism of ; :: thesis: f is Morphism of a,b
f in Hom a,b by Th52;
hence f is Morphism of a,b by CAT_1:def 7; :: thesis: verum