set c = the Object of C;
set E = 1Cat ( the Object of C,(id the Object of C));
now :: thesis: ( the carrier of (1Cat ( the Object of C,(id the Object of C))) c= the carrier of C & ( for a, b being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )
thus the carrier of (1Cat ( the Object of C,(id the Object of C))) c= the carrier of C :: thesis: ( ( for a, b being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (1Cat ( the Object of C,(id the Object of C))) or a in the carrier of C )
assume a in the carrier of (1Cat ( the Object of C,(id the Object of C))) ; :: thesis: a in the carrier of C
then a = the Object of C by TARSKI:def 1;
hence a in the carrier of C ; :: thesis: verum
end;
thus for a, b being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) :: thesis: ( the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C & ( for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9 ) )
proof
let a, b be Object of (1Cat ( the Object of C,(id the Object of C))); :: thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of C; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) c= Hom (a9,b9)
then A1: ( a9 = the Object of C & b9 = the Object of C ) by TARSKI:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume x in Hom (a,b) ; :: thesis: x in Hom (a9,b9)
then x = id the Object of C by TARSKI:def 1;
hence x in Hom (a9,b9) by A1, CAT_1:27; :: thesis: verum
end;
thus the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C :: thesis: for a being Object of (1Cat ( the Object of C,(id the Object of C)))
for a9 being Object of C st a = a9 holds
id a = id a9
proof
reconsider i = id the Object of C as Morphism of C ;
A2: Hom ( the Object of C, the Object of C) <> {} ;
A3: ( dom (id the Object of C) = the Object of C & cod (id the Object of C) = the Object of C ) ;
then A4: [(id the Object of C),(id the Object of C)] in dom the Comp of C by CAT_1:15;
the Comp of (1Cat ( the Object of C,(id the Object of C))) = ((id the Object of C),(id the Object of C)) .--> ((id the Object of C) * (id the Object of C))
.= ((id the Object of C),(id the Object of C)) .--> ((id the Object of C) (*) i) by A2, CAT_1:def 13
.= [(id the Object of C),(id the Object of C)] .--> ( the Comp of C . ((id the Object of C),(id the Object of C))) by A3, CAT_1:16 ;
hence the Comp of (1Cat ( the Object of C,(id the Object of C))) c= the Comp of C by A4, FUNCT_4:7; :: thesis: verum
end;
let a be Object of (1Cat ( the Object of C,(id the Object of C))); :: thesis: for a9 being Object of C st a = a9 holds
id a = id a9
let a9 be Object of C; :: thesis: ( a = a9 implies id a = id a9 )
assume a = a9 ; :: thesis: id a = id a9
then a9 = the Object of C by TARSKI:def 1;
hence id a = id a9 by TARSKI:def 1; :: thesis: verum
end;
then 1Cat ( the Object of C,(id the Object of C)) is Subcategory of C by Def4;
hence ex b1 being Subcategory of C st b1 is strict ; :: thesis: verum