let o, m be set ; :: thesis: for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b
let a, b be Object of (1Cat (o,m)); :: thesis: for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b
let f be Morphism of (1Cat (o,m)); :: thesis: f is Morphism of a,b
f in Hom (a,b) by Th9;
hence f is Morphism of a,b by Def3; :: thesis: verum