A1: now :: thesis: for a being Object of (1Cat (c,(id c)))
for c1 being Object of C st a = c1 holds
id a = id c1
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 :: thesis: for a, b being Object of (1Cat (c,(id c)))
for c1, c2 being Object of C st a = c1 & b = c2 holds
Hom (a,b) c= Hom (c1,c2)
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 Th4, CAT_1:27;
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:31; :: 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:13;
A5: dom (id c) = c ;
A6: cod (id c) = c ;
A7: (((id c),(id c)) .--> (id c)) . ((id c),(id c)) = id c by FUNCOP_1:71;
A8: now :: thesis: for x being object st x in dom the Comp of (1Cat (c,(id c))) holds
the Comp of (1Cat (c,(id c))) . x = the Comp of C . x
let x be object ; :: 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:21
.= the Comp of C . ((id c),(id c)) by A5, A6, CAT_1:16
.= 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:15;
then dom the Comp of (1Cat (c,(id c))) c= dom the Comp of C by A4, ZFMISC_1:31;
then ( H1( 1Cat (c,(id c))) = {c} & the Comp of (1Cat (c,(id c))) c= the Comp of C ) by A8, GRFUNC_1:2;
hence 1Cat (c,(id c)) is strict Subcategory of C by A2, A1, CAT_2:def 4; :: thesis: verum