let o, m be set ; :: thesis: for a, b being Object of (c1Cat o,m)
for f being Morphism of (c1Cat o,m) holds f in Hom a,b
let a, b be Object of (c1Cat o,m); :: thesis: for f being Morphism of (c1Cat o,m) holds f in Hom a,b
let f be Morphism of (c1Cat o,m); :: thesis: f in Hom a,b
( dom f = o & cod 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