let o, m be set ; :: thesis: for a, b, c, d being Object of (1Cat o,m)
for f being Morphism of a,b
for g being Morphism of c,d holds f = g
let a, b, c, d be Object of (1Cat o,m); :: thesis: for f being Morphism of a,b
for g being Morphism of c,d holds f = g
let f be Morphism of a,b; :: thesis: for g being Morphism of c,d holds f = g
let g be Morphism of c,d; :: thesis: f = g
( f = m & g = m ) by TARSKI:def 1;
hence f = g ; :: thesis: verum