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