consider a being Object of C;
A1: dom (Obj F) = the carrier of C by FUNCT_2:def 1;
then (Obj F) . a in rng (Obj F) by FUNCT_1:def 5;
then reconsider O = rng (Obj F) as non empty set ;
reconsider O = O as non empty Subset of the carrier of D ;
consider f being Morphism of C;
A2: dom F = the carrier' of C by FUNCT_2:def 1;
A3: dom the Source of D = the carrier' of D by FUNCT_2:def 1;
A4: dom the Target of D = the carrier' of D by FUNCT_2:def 1;
A5: dom the Id of D = the carrier of D by FUNCT_2:def 1;
defpred S₁[ set ] means ( rng F c= $1 & ex E being Subcategory of D st
( the carrier of E = O & the carrier' of E = $1 ) );
consider MM being set such that
A6: for x being set holds
( x in MM iff ( x in bool the carrier' of D & S₁[x] ) ) from XBOOLE_0:sch 1();
set HH = { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } ;
reconsider M0 = union { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } as non empty Subset of the carrier' of D by CAT_2:28;
reconsider D0 = the Source of D | M0, C0 = the Target of D | M0 as Function of M0,O by CAT_2:29;
reconsider CC = the Comp of D || M0 as PartFunc of [:M0,M0:],M0 by CAT_2:29;
reconsider I0 = the Id of D | O as Function of O,M0 by CAT_2:29;
CatStr(# O,M0,D0,C0,CC,I0 #) is_full_subcategory_of D by CAT_2:30;
then A7: CatStr(# O,M0,D0,C0,CC,I0 #) is Subcategory of D by CAT_2:def 6;
rng F c= M0

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in M0 )
assume y in rng F ; :: thesis: y in M0
then consider x being set such that
A8: x in dom F and
A9: y = F . x by FUNCT_1:def 5;
reconsider x = x as Morphism of C by A8;
A10: (Obj F) . (dom x) in O by A1, FUNCT_1:def 5;
A11: (Obj F) . (cod x) in O by A1, FUNCT_1:def 5;
A12: dom (F . x) in O by A10, CAT_1:105;
A13: cod (F . x) in O by A11, CAT_1:105;
A14: y in Hom ((dom (F . x)),(cod (F . x))) by A9;
Hom ((dom (F . x)),(cod (F . x))) in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by A12, A13;
hence y in M0 by A14, TARSKI:def 4; :: thesis: verum

end;

then A15: M0 in MM by A6, A7;
set M = meet MM;
A16: for Z being set st Z in MM holds
rng F c= Z by A6;
then A17: rng F c= meet MM by A15, SETFAM_1:6;

now

let X be set ; :: thesis: ( X in MM implies F . f in X )
assume X in MM ; :: thesis: F . f in X
then A18: rng F c= X by A6;
F . f in rng F by A2, FUNCT_1:def 5;
hence F . f in X by A18; :: thesis: verum

end;

then reconsider M = meet MM as non empty set by A15, SETFAM_1:def 1;
M c= the carrier' of D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in M or x in the carrier' of D )
assume x in M ; :: thesis: x in the carrier' of D
then x in M0 by A15, SETFAM_1:def 1;
hence x in the carrier' of D ; :: thesis: verum

end;

then reconsider M = M as non empty Subset of the carrier' of D ;
set DOM = the Source of D | M;
set COD = the Target of D | M;
set COMP = the Comp of D || M;
set ID = the Id of D | O;
A19: dom ( the Source of D | M) = M by A3, RELAT_1:91;
rng ( the Source of D | M) c= O

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Source of D | M) or y in O )
assume y in rng ( the Source of D | M) ; :: thesis: y in O
then consider x being set such that
A20: x in M and
A21: y = ( the Source of D | M) . x by A19, FUNCT_1:def 5;
reconsider x = x as Morphism of D by A20;
x in M0 by A15, A20, SETFAM_1:def 1;
then consider X being set such that
A22: x in X and
A23: X in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by TARSKI:def 4;
consider a, b being Object of D such that
A24: X = Hom (a,b) and
A25: a in O and
b in O by A23;
dom x = a by A22, A24, CAT_1:18;
hence y in O by A19, A20, A21, A25, FUNCT_1:70; :: thesis: verum

end;

then reconsider DOM = the Source of D | M as Function of M,O by A19, FUNCT_2:def 1, RELSET_1:11;
A26: dom ( the Target of D | M) = M by A4, RELAT_1:91;
rng ( the Target of D | M) c= O

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Target of D | M) or y in O )
assume y in rng ( the Target of D | M) ; :: thesis: y in O
then consider x being set such that
A27: x in M and
A28: y = ( the Target of D | M) . x by A26, FUNCT_1:def 5;
reconsider x = x as Morphism of D by A27;
x in M0 by A15, A27, SETFAM_1:def 1;
then consider X being set such that
A29: x in X and
A30: X in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by TARSKI:def 4;
consider a, b being Object of D such that
A31: X = Hom (a,b) and
a in O and
A32: b in O by A30;
cod x = b by A29, A31, CAT_1:18;
hence y in O by A26, A27, A28, A32, FUNCT_1:70; :: thesis: verum

end;

then reconsider COD = the Target of D | M as Function of M,O by A26, FUNCT_2:def 1, RELSET_1:11;
A33: dom ( the Comp of D || M) c= [:M,M:] by RELAT_1:87;
rng ( the Comp of D || M) c= M

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Comp of D || M) or y in M )
assume y in rng ( the Comp of D || M) ; :: thesis: y in M
then consider x being set such that
A34: x in dom ( the Comp of D || M) and
A35: y = ( the Comp of D || M) . x by FUNCT_1:def 5;
reconsider x1 = x `1 , x2 = x `2 as Element of M by A33, A34, MCART_1:10;
A36: x = [x1,x2] by A33, A34, MCART_1:23;

now

let X be set ; :: thesis: ( X in MM implies y in X )
assume A37: X in MM ; :: thesis: y in X
then consider E being Subcategory of D such that
the carrier of E = O and
A38: the carrier' of E = X by A6;
reconsider y1 = x1, y2 = x2 as Morphism of E by A37, A38, SETFAM_1:def 1;
dom ( the Comp of D || M) = (dom the Comp of D) /\ [:M,M:] by RELAT_1:90;
then x in dom the Comp of D by A34, XBOOLE_0:def 4;
then A39: dom x1 = cod x2 by A36, CAT_1:40;
A40: dom y1 = dom x1 by CAT_2:15;
cod y2 = cod x2 by CAT_2:15;
then A41: x in dom the Comp of E by A36, A39, A40, CAT_1:40;
the Comp of E c= the Comp of D by CAT_2:def 4;
then the Comp of E . x = the Comp of D . x by A41, GRFUNC_1:8
.= y by A34, A35, FUNCT_1:70 ;
then y in rng the Comp of E by A41, FUNCT_1:def 5;
hence y in X by A38; :: thesis: verum

end;

hence y in M by A15, SETFAM_1:def 1; :: thesis: verum

end;

then reconsider COMP = the Comp of D || M as PartFunc of [:M,M:],M by A33, RELSET_1:11;
A42: dom ( the Id of D | O) = O by A5, RELAT_1:91;
rng ( the Id of D | O) c= M

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Id of D | O) or y in M )
assume y in rng ( the Id of D | O) ; :: thesis: y in M
then consider x being set such that
A43: x in O and
A44: y = ( the Id of D | O) . x by A42, FUNCT_1:def 5;
reconsider x = x as Object of D by A43;
consider x9 being set such that
A45: x9 in dom (Obj F) and
A46: x = (Obj F) . x9 by A43, FUNCT_1:def 5;
reconsider x9 = x9 as Object of C by A45;
y = id x by A42, A43, A44, FUNCT_1:70
.= F . (id x9) by A46, CAT_1:104 ;
then y in rng F by A2, FUNCT_1:def 5;
hence y in M by A17; :: thesis: verum

end;

then reconsider ID = the Id of D | O as Function of O,M by A42, FUNCT_2:def 1, RELSET_1:11;
reconsider T = CatStr(# O,M,DOM,COD,COMP,ID #) as strict Subcategory of D by NATTRA_1:9;
take T ; :: thesis: ( the carrier of T = rng (Obj F) & rng F c= the carrier' of T & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
T is Subcategory of E ) )
thus ( the carrier of T = rng (Obj F) & rng F c= the carrier' of T ) by A15, A16, SETFAM_1:6; :: thesis: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
T is Subcategory of E
let E be Subcategory of D; :: thesis: ( the carrier of E = rng (Obj F) & rng F c= the carrier' of E implies T is Subcategory of E )
assume that
A47: the carrier of E = rng (Obj F) and
A48: rng F c= the carrier' of E ; :: thesis: T is Subcategory of E
thus the carrier of T c= the carrier of E by A47; :: according to CAT_2:def 4 :: thesis: ( ( for b₁, b₂ being Element of the carrier of T
for b₃, b₄ being Element of the carrier of E holds
( not b₁ = b₃ or not b₂ = b₄ or Hom (b₁,b₂) c= Hom (b₃,b₄) ) ) & the Comp of T c= the Comp of E & ( for b₁ being Element of the carrier of T
for b₂ being Element of the carrier of E holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )
the carrier' of E c= the carrier' of D by CAT_2:13;
then the carrier' of E in MM by A6, A47, A48;
then A49: M c= the carrier' of E by SETFAM_1:4;

hereby :: thesis: ( the Comp of T c= the Comp of E & ( for b₁ being Element of the carrier of T
for b₂ being Element of the carrier of E holds
( not b₁ = b₂ or id b₁ = id b₂ ) ) )

let a, b be Object of T; :: thesis: for a9, b9 being Object of E st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of E; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that
A50: a = a9 and
A51: b = b9 ; :: thesis: Hom (a,b) c= Hom (a9,b9)
thus Hom (a,b) c= Hom (a9,b9) :: thesis: verum

proof

let x be set ; :: 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 consider f being Morphism of T such that
A52: x = f and
A53: dom f = a and
A54: cod f = b ;
reconsider g = f as Morphism of D by TARSKI:def 3;
reconsider f = f as Morphism of E by A49, TARSKI:def 3;
A55: dom g = a by A53, CAT_2:15;
A56: cod g = b by A54, CAT_2:15;
A57: a9 = dom f by A50, A55, CAT_2:15;
b9 = cod f by A51, A56, CAT_2:15;
hence x in Hom (a9,b9) by A52, A57; :: thesis: verum

end;

end;

A58: dom the Comp of T c= dom the Comp of E

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of T or x in dom the Comp of E )
assume A59: x in dom the Comp of T ; :: thesis: x in dom the Comp of E
then reconsider x1 = x `1 , x2 = x `2 as Element of M by MCART_1:10;
reconsider y1 = x1, y2 = x2 as Morphism of T ;
reconsider z1 = x1, z2 = x2 as Morphism of E by A49, TARSKI:def 3;
A60: x = [x1,x2] by A59, MCART_1:23;
then A61: dom y1 = cod y2 by A59, CAT_1:40;
A62: dom y1 = dom x1 by CAT_2:15;
A63: dom z1 = dom x1 by CAT_2:15;
A64: cod y2 = cod x2 by CAT_2:15;
cod z2 = cod x2 by CAT_2:15;
hence x in dom the Comp of E by A60, A61, A62, A63, A64, CAT_1:40; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom the Comp of T implies the Comp of T . x = the Comp of E . x )
assume A65: x in dom the Comp of T ; :: thesis: the Comp of T . x = the Comp of E . x
A66: the Comp of T c= the Comp of D by CAT_2:def 4;
A67: the Comp of E c= the Comp of D by CAT_2:def 4;
thus the Comp of T . x = the Comp of D . x by A65, A66, GRFUNC_1:8
.= the Comp of E . x by A58, A65, A67, GRFUNC_1:8 ; :: thesis: verum

end;

hence the Comp of T c= the Comp of E by A58, GRFUNC_1:8; :: thesis: for b₁ being Element of the carrier of T
for b₂ being Element of the carrier of E holds
( not b₁ = b₂ or id b₁ = id b₂ )
let a be Object of T; :: thesis: for b₁ being Element of the carrier of E holds
( not a = b₁ or id a = id b₁ )
let a9 be Object of E; :: thesis: ( not a = a9 or id a = id a9 )
reconsider b = a as Object of D by TARSKI:def 3;
assume A68: a = a9 ; :: thesis: id a = id a9
id a = id b by CAT_2:def 4;
hence id a = id a9 by A68, CAT_2:def 4; :: thesis: verum