A1: H₁( 1Cat c,(id c)) = {c} ;

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
( a = c & b = c & id c in Hom c,c & Hom a,a = {(id c)} ) by Th5, CAT_1:55, TARSKI:def 1;
hence for c1, c2 being Object of C st a = c1 & b = c2 holds
Hom a,b c= Hom c1,c2 by ZFMISC_1:37; :: thesis: verum

end;

set m = id c;
set s = (id c),(id c) .--> (id c);
A3: ((id c),(id c) .--> (id c)) . (id c),(id c) = id c by FUNCOP_1:86;
A4: dom ((id c),(id c) .--> (id c)) = {[(id c),(id c)]} by FUNCOP_1:19;
A5: ( dom (id c) = c & cod (id c) = c ) by CAT_1:44;
then [(id c),(id c)] in dom the Comp of C by CAT_1:40;
then A6: dom the Comp of (1Cat c,(id c)) c= dom the Comp of C by A4, ZFMISC_1:37;

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 A7: 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 A3, A4, TARSKI:def 1
.= (id c) * (id c) by A5, CAT_1:46
.= the Comp of C . (id c),(id c) by A5, CAT_1:41
.= the Comp of C . x by A4, A7, TARSKI:def 1 ;
:: thesis: verum

end;

then A8: the Comp of (1Cat c,(id c)) c= the Comp of C by A6, GRFUNC_1:8;

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 & a = c ) by TARSKI:def 1;
hence for c1 being Object of C st a = c1 holds
id a = id c1 ; :: thesis: verum

end;

hence 1Cat c,(id c) is strict Subcategory of C by A1, A2, A8, CAT_2:def 4; :: thesis: verum