let o, m be object ; :: thesis: for c being Element of (1Cat (o,m)) holds
( c is Object of (1Cat (o,m)) & c = o & id c = m )
let c be Element of (1Cat (o,m)); :: thesis: ( c is Object of (1Cat (o,m)) & c = o & id c = m )
reconsider o9 = o, m9 = m as set by TARSKI:1;
set C = 1Cat (o,m);
A1: 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) by CAT_1:def 11;
hence ( c is Object of (1Cat (o,m)) & c = o ) by TARSKI:def 1; :: thesis: id c = m
o9 is Object of (1Cat (o9,m9)) by A1, TARSKI:def 1;
then A2: Hom (c,c) = {m} by COMMACAT:4;
id c in Hom (c,c) by CAT_1:27;
hence id c = m by A2, TARSKI:def 1; :: thesis: verum