set c = the Object of C;

set E = 1Cat ( the Object of C,(id the Object of C));

hence ex b_{1} being Subcategory of C st b_{1} is strict
; :: thesis: verum

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 ) )

then
1Cat ( the Object of C,(id the Object of C)) is Subcategory of C
by Def4;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 ) )

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 ) )

for a9 being Object of C st a = a9 holds

id a = id a9

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;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

thus
for a, b being Object of (1Cat ( the Object of C,(id the Object of C)))
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;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

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

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)))
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;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

for a9 being Object of C st a = a9 holds

id a = id a9

proof

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
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;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

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

hence ex b