let o, m be set ; :: thesis: for f, g being Morphism of (c1Cat o,m) holds f = g
let f, g be Morphism of (c1Cat o,m); :: thesis: f = g
( f = m & g = m ) by TARSKI:def 1;
hence f = g ; :: thesis: verum