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 by TARSKI:def 1;
hence f = g by TARSKI:def 1; :: thesis: verum