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