let o, m be object ; :: thesis: for c being Object of (1Cat (o,m)) holds c = o
let c be Object of (1Cat (o,m)); :: thesis: c = o
set C = 1Cat (o,m);
1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) by CAT_1:def 11;
hence c = o by TARSKI:def 1; :: thesis: verum