A1: now

let a be Object of (1Cat (c,(id c))); :: thesis: for c1 being Object of C st a = c1 holds
id a = id c1
id a = id c by TARSKI:def 1;
hence for c1 being Object of C st a = c1 holds
id a = id c1 by TARSKI:def 1; :: thesis: verum

end;

A2: now

let a, b be Object of (1Cat (c,(id c))); :: thesis: for c1, c2 being Object of C st a = c1 & b = c2 holds
Hom (a,b) c= Hom (c1,c2)
A3: ( a = c & b = c ) by TARSKI:def 1;
( id c in Hom (c,c) & Hom (a,a) = {(id c)} ) by Th5, CAT_1:55;
hence for c1, c2 being Object of C st a = c1 & b = c2 holds
Hom (a,b) c= Hom (c1,c2) by A3, ZFMISC_1:37; :: thesis: verum

end;

set m = id c;
set s = ((id c),(id c)) .--> (id c);
A4: dom (((id c),(id c)) .--> (id c)) = {[(id c),(id c)]} by FUNCOP_1:19;
A5: dom (id c) = c by CAT_1:44;
A6: cod (id c) = c by CAT_1:44;
A7: (((id c),(id c)) .--> (id c)) . ((id c),(id c)) = id c by FUNCOP_1:86;

A8: now

let x be set ; :: thesis: ( x in dom the Comp of (1Cat (c,(id c))) implies the Comp of (1Cat (c,(id c))) . x = the Comp of C . x )
assume A9: x in dom the Comp of (1Cat (c,(id c))) ; :: thesis: the Comp of (1Cat (c,(id c))) . x = the Comp of C . x
hence the Comp of (1Cat (c,(id c))) . x = id c by A7, A4, TARSKI:def 1
.= (id c) * (id c) by A6, CAT_1:46
.= the Comp of C . ((id c),(id c)) by A5, A6, CAT_1:41
.= the Comp of C . x by A4, A9, TARSKI:def 1 ;
:: thesis: verum

end;

[(id c),(id c)] in dom the Comp of C by A5, A6, CAT_1:40;
then dom the Comp of (1Cat (c,(id c))) c= dom the Comp of C by A4, ZFMISC_1:37;
then ( H₁( 1Cat (c,(id c))) = {c} & the Comp of (1Cat (c,(id c))) c= the Comp of C ) by A8, GRFUNC_1:8;
hence 1Cat (c,(id c)) is strict Subcategory of C by A2, A1, CAT_2:def 4; :: thesis: verum