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 in Hom (a,b)
let a, b be Object of (1Cat (o,m)); :: thesis: for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)
let f be Morphism of (1Cat (o,m)); :: thesis: f in Hom (a,b)
dom f = o by TARSKI:def 1;
then ( dom f = a & cod f = b ) by TARSKI:def 1;
hence f in Hom (a,b) ; :: thesis: verum