let o, m be set ; :: thesis: for a, b being Object of
for f being Morphism of holds f in Hom a,b
let a, b be Object of ; :: thesis: for f being Morphism of holds f in Hom a,b
let f be Morphism of ; :: thesis: f in Hom a,b
cod f = o by TARSKI:def 1;
then A1: cod f = b by TARSKI:def 1;
dom f = o by TARSKI:def 1;
then dom f = a by TARSKI:def 1;
hence f in Hom a,b by A1; :: thesis: verum