deffunc H₁( Object of C) -> Morphism of $1,$1 = id $1;
defpred S₁[ Object of C] means verum;
defpred S₂[ Object of C] means H₁($1) in the carrier' of C;
set M = { H₁(a) where a is Object of C : S₁[a] } ;
set N = { H₁(a) where a is Object of C : S₂[a] } ;
A1: for a being Object of C holds
( S₂[a] iff S₁[a] ) ;
A2: { H₁(a) where a is Object of C : S₂[a] } = { H₁(a) where a is Object of C : S₁[a] } from FRAENKEL:sch 3(A1);
set N' = { H₁(a) where a is Object of C : ( H₁(a) in the carrier' of C & S₁[a] ) } ;
A3: { H₁(a) where a is Object of C : ( H₁(a) in the carrier' of C & S₁[a] ) } c= the carrier' of C from FRAENKEL:sch 17();
defpred S₃[ Object of C] means ( H₁($1) in the carrier' of C & S₁[$1] );
set N'' = { H₁(a) where a is Object of C : S₃[a] } ;
A4: for a being Object of C holds
( S₂[a] iff S₃[a] ) ;
A5: { H₁(a) where a is Object of C : S₂[a] } = { H₁(a) where a is Object of C : S₃[a] } from FRAENKEL:sch 3(A4);
consider a being Object of C;
id a in { H₁(a) where a is Object of C : S₁[a] } ;
then reconsider M = { H₁(a) where a is Object of C : S₁[a] } as non empty Subset of the carrier' of C by A2, A3, A5;
A6: the Comp of C || M is PartFunc of [:M,M:],the carrier' of C by PARTFUN1:43;
rng (the Comp of C || M) c= M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (the Comp of C || M) or x in M )
assume x in rng (the Comp of C || M) ; :: thesis: x in M
then consider y being set such that
A7: y in dom (the Comp of C || M) and
A8: x = (the Comp of C || M) . y by FUNCT_1:def 5;
A9: y in (dom the Comp of C) /\ [:M,M:] by A7, RELAT_1:90;
then y in [:M,M:] by XBOOLE_0:def 4;
then consider y1, y2 being set such that
A10: ( y1 in M & y2 in M ) and
A11: y = [y1,y2] by ZFMISC_1:103;
consider a1 being Object of C such that
A12: y1 = id a1 by A10;
consider a2 being Object of C such that
A13: y2 = id a2 by A10;
A14: y in dom the Comp of C by A9, XBOOLE_0:def 4;
A15: Hom a1,a1 <> {} by CAT_1:56;
A16: a1 = dom (id a1) by CAT_1:44
.= cod (id a2) by A11, A12, A13, A14, CAT_1:40
.= a2 by CAT_1:44 ;
id a1 = (id a1) * (id a1) by CAT_1:59
.= (id a1) * (id a2) by A15, A16, CAT_1:def 13
.= the Comp of C . (id a1),(id a2) by A11, A12, A13, A14, CAT_1:def 4
.= x by A8, A9, A11, A12, A13, FUNCT_1:71 ;
hence x in M ; :: thesis: verum

end;

then reconsider COMP = the Comp of C || M as PartFunc of [:M,M:],M by A6, RELSET_1:14;
A17: dom the Id of C = the carrier of C by FUNCT_2:def 1;
rng the Id of C c= M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Id of C or x in M )
assume x in rng the Id of C ; :: thesis: x in M
then consider y being set such that
A18: y in dom the Id of C and
A19: x = the Id of C . y by FUNCT_1:def 5;
reconsider y = y as Object of C by A18, FUNCT_2:def 1;
x = id y by A19;
hence x in M ; :: thesis: verum

end;

then reconsider ID = the Id of C as Function of the carrier of C,M by A17, FUNCT_2:4;
dom the Id of C = the carrier of C by FUNCT_2:def 1;
then A20: the Id of C | the carrier of C = the Id of C by RELAT_1:97;
the carrier of C c= the carrier of C ;
then reconsider A = CatStr(# the carrier of C,M,(the Source of C | M),(the Target of C | M),COMP,ID #) as Subcategory of C by A20, Th9;

now

let f be Morphism of A; :: thesis: ex a being Object of A st f = id a
f in M ;
then consider a being Object of C such that
A21: f = id a ;
reconsider a = a as Object of A ;
take a = a; :: thesis: f = id a
thus f = id a by A21; :: thesis: verum

end;

then reconsider A = A as strict discrete Subcategory of C by Def19;
take A ; :: thesis: ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } )
thus ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } ) ; :: thesis: verum