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