let o, m be set ; :: thesis: for a, b being Object of (c1Cat* (o,m)) holds a = b
let a, b be Object of (c1Cat* (o,m)); :: thesis: a = b
a = o by TARSKI:def 1;
hence a = b by TARSKI:def 1; :: thesis: verum