let M be non empty MetrSpace; :: thesis:
let S be non empty compact TopSpace; :: thesis:
let T be non empty MetrSpace; :: thesis:
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis:
let H be non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)); :: thesis:
assume A1: ( S = TopSpaceMetr M & T is complete ) ; :: thesis:
assume A2: G = H ; :: thesis:
set Z = MetricSpace_of_ContinuousFunctions (S,T);
set MZH = (MetricSpace_of_ContinuousFunctions (S,T)) | H;
A3: the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) = H by TOPMETR:def 2;

hereby :: thesis:

assume A4: (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded ; :: thesis:
hence G is equicontinuous by Th16, A1, A2; :: thesis:
thus for x being Point of S
for Hx being non empty Subset of T st Hx = { (f . x) where f is Function of S,T : f in H } holds
T | (Cl Hx) is compact :: thesis:

let x be Point of S; :: thesis:
let Hx be non empty Subset of T; :: thesis:
assume A5: Hx = { (f . x) where f is Function of S,T : f in H } ; :: thesis:
T | Hx is totally_bounded by Th16, A1, A2, A4, A5;
hence T | (Cl Hx) is compact by Th5, A1; :: thesis:

end;

assume A6: ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of T st Hx = { (f . x) where f is Function of S,T : f in H } holds
T | (Cl Hx) is compact ) ) ; :: thesis:
for e being Real st e > 0 holds
ex L being Subset-Family of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
( L is finite & the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) = union L & ( for C being Subset of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st C in L holds
ex w being Element of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st C = Ball (w,e) ) )

proof

let e0 be Real; :: thesis:
assume A7: e0 > 0 ; :: thesis:
then A8: ( 0 < e0 / 2 & e0 / 2 < e0 ) by XREAL_1:216;
set e = e0 / 2;
consider d being Real such that
A9: ( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
dist ((f . x1),(f . x2)) < (e0 / 2) / 4 ) ) by A6, A7;
set BM = { (Ball (x0,d)) where x0 is Element of M : verum } ;
{ (Ball (x0,d)) where x0 is Element of M : verum } c= bool the carrier of S

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { (Ball (x0,d)) where x0 is Element of M : verum } ; :: thesis:
then consider x0 being Point of M such that
A10: z = Ball (x0,d) ;
thus z in bool the carrier of S by A10, A1; :: thesis:

end;

then reconsider BM = { (Ball (x0,d)) where x0 is Element of M : verum } as Subset-Family of S ;
for P being Subset of S st P in BM holds
P is open

proof

let P be Subset of S; :: thesis:
assume P in BM ; :: thesis:
then consider x0 being Point of M such that
A11: P = Ball (x0,d) ;
thus P is open by A1, A11, PCOMPS_1:29; :: thesis:

end;

then A12: BM is open by TOPS_2:def 1;
the carrier of S c= union BM

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in the carrier of S ; :: thesis:
then reconsider x0 = z as Point of M by A1;
A13: Ball (x0,d) in BM ;
dist (x0,x0) < d by A9, METRIC_1:1;
then x0 in { y where y is Element of M : dist (x0,y) < d } ;
then x0 in Ball (x0,d) by METRIC_1:def 14;
hence z in union BM by TARSKI:def 4, A13; :: thesis:

end;

then BM is Cover of [#] S by SETFAM_1:def 11;
then consider BM0 being Subset-Family of S such that
A14: ( BM0 c= BM & BM0 is Cover of [#] S & BM0 is finite ) by COMPTS_1:def 4, COMPTS_1:1, A12;
reconsider BM0 = BM0 as finite set by A14;
defpred S₁[ object , object ] means ex w being Point of M st
( $2 = w & $1 = Ball (w,d) );
A15: for D being object st D in BM holds
ex w being object st
( w in the carrier of M & S₁[D,w] )

proof

let D be object ; :: thesis:
assume D in BM ; :: thesis:
then consider w being Element of M such that
A16: D = Ball (w,d) ;
take w ; :: thesis:
thus ( w in the carrier of M & S₁[D,w] ) by A16; :: thesis:

end;

consider U being Function of BM, the carrier of M such that
A17: for D being object st D in BM holds
S₁[D,U . D] from FUNCT_2:sch 1(A15);
A18: for D being object st D in BM holds
D = Ball ((U /. D),d)

proof

let D be object ; :: thesis:
assume A19: D in BM ; :: thesis:
then A20: ex x0 being Point of M st
( U . D = x0 & D = Ball (x0,d) ) by A17;
dom U = BM by FUNCT_2:def 1;
hence D = Ball ((U /. D),d) by A20, A19, PARTFUN1:def 6; :: thesis:

end;

set CF = canFS BM0;
A21: len (canFS BM0) = card BM0 by FINSEQ_1:93;
A22: rng (canFS BM0) = BM0 by FUNCT_2:def 3;
A23: dom U = BM by FUNCT_2:def 1;
then reconsider PS = U * (canFS BM0) as FinSequence by A22, A14, FINSEQ_1:16;
rng PS c= rng U by RELAT_1:26;
then reconsider PS = PS as FinSequence of the carrier of S by FINSEQ_1:def 4, A1, XBOOLE_1:1;
A24: dom PS = dom (canFS BM0) by A22, A23, A14, RELAT_1:27
.= Seg (card BM0) by A21, FINSEQ_1:def 3 ;
A25: dom (canFS BM0) = Seg (len (canFS BM0)) by FINSEQ_1:def 3
.= dom PS by A24, FINSEQ_1:93 ;
A26: for i being Nat st i in dom PS holds
(canFS BM0) . i = Ball (((U * (canFS BM0)) /. i),d)

proof

let i be Nat; :: thesis:
assume A27: i in dom PS ; :: thesis:
then A28: (canFS BM0) . i in rng (canFS BM0) by FUNCT_1:3, A25;
then U /. ((canFS BM0) . i) = U . ((canFS BM0) . i) by PARTFUN1:def 6, A23, A14
.= PS . i by FUNCT_1:12, A27
.= (U * (canFS BM0)) /. i by PARTFUN1:def 6, A27 ;
hence (canFS BM0) . i = Ball (((U * (canFS BM0)) /. i),d) by A28, A18, A14; :: thesis:

end;

union (rng (canFS BM0)) = union BM0 by FUNCT_2:def 3;
then A29: the carrier of S c= union (rng (canFS BM0)) by A14, SETFAM_1:def 11;
A30: BM0 <> {}

proof

assume BM0 = {} ; :: thesis:
then [#] S c= {} by SETFAM_1:def 11, A14, ZFMISC_1:2;
hence contradiction ; :: thesis:

end;

defpred S₂[ object , object ] means ex x being Point of S ex NHx, CHx being non empty Subset of T st
( $1 = x & NHx = { (f . x) where f is Function of S,T : f in H } & $2 = Cl NHx );
A31: for x being object st x in the carrier of S holds
ex B being object st
( B in bool the carrier of T & S₂[x,B] )

proof

let x be object ; :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider x0 = x as Point of S ;
set NHx = { (f . x0) where f is Function of S,T : f in H } ;
consider f0 being object such that
A32: f0 in H by XBOOLE_0:def 1;
f0 in MetricSpace_of_ContinuousFunctions (S,T) by A32;
then ex g being Function of the carrier of S,(TopSpaceMetr T) st
( f0 = g & g is continuous ) ;
then reconsider g = f0 as Function of S,T ;
A33: g . x0 in { (f . x0) where f is Function of S,T : f in H } by A32;
{ (f . x0) where f is Function of S,T : f in H } c= the carrier of T

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { (f . x0) where f is Function of S,T : f in H } ; :: thesis:
then consider f being Function of S,T such that
A34: ( z = f . x0 & f in H ) ;
thus z in the carrier of T by A34; :: thesis:

end;

then reconsider NHx = { (f . x0) where f is Function of S,T : f in H } as non empty Subset of T by A33;
reconsider CHx = Cl NHx as non empty Subset of T ;
CHx in bool the carrier of T ;
hence ex B being object st
( B in bool the carrier of T & S₂[x,B] ) ; :: thesis:

end;

consider ST being Function of the carrier of S,(bool the carrier of T) such that
A35: for x being object st x in the carrier of S holds
S₂[x,ST . x] from FUNCT_2:sch 1(A31);
A36: dom ST = the carrier of S by FUNCT_2:def 1;
A37: rng PS c= the carrier of S ;
then reconsider STPS = ST * PS as FinSequence by A36, FINSEQ_1:16;
rng STPS c= rng ST by RELAT_1:26;
then reconsider STPS = STPS as FinSequence of bool the carrier of (TopSpaceMetr T) by FINSEQ_1:def 4, XBOOLE_1:1;
A38: dom STPS = Seg (card BM0) by A24, A36, A37, RELAT_1:27;
A39: for i being Nat st i in dom STPS holds
( ex NHx, CHx being non empty Subset of T st
( NHx = { (f . (PS /. i)) where f is Function of S,T : f in H } & STPS /. i = Cl NHx ) & not STPS /. i is empty )

proof

let i be Nat; :: thesis:
assume A40: i in dom STPS ; :: thesis:
then A41: STPS /. i = STPS . i by PARTFUN1:def 6
.= ST . (PS . i) by FUNCT_1:12, A40 ;
consider x being Point of S, NHx, CHx being non empty Subset of T such that
A42: ( PS /. i = x & NHx = { (f . x) where f is Function of S,T : f in H } & ST . (PS /. i) = Cl NHx ) by A35;
A43: STPS /. i = Cl NHx by A42, A41, A38, A24, A40, PARTFUN1:def 6;
consider f0 being object such that
A44: f0 in H by XBOOLE_0:def 1;
f0 in MetricSpace_of_ContinuousFunctions (S,T) by A44;
then ex g being Function of S,(TopSpaceMetr T) st
( f0 = g & g is continuous ) ;
then reconsider g = f0 as Function of S,T ;
thus ( ex NHx, CHx being non empty Subset of T st
( NHx = { (f . (PS /. i)) where f is Function of S,T : f in H } & STPS /. i = Cl NHx ) & not STPS /. i is empty ) by A42, A43; :: thesis:

end;

for i being Nat st i in Seg (len STPS) holds
STPS /. i is compact

proof

let i be Nat; :: thesis:
assume i in Seg (len STPS) ; :: thesis:
then i in dom STPS by FINSEQ_1:def 3;
then consider NHx, CHx being non empty Subset of T such that
A45: ( NHx = { (f . (PS /. i)) where f is Function of S,T : f in H } & STPS /. i = Cl NHx ) by A39;
reconsider Hx1 = NHx as non empty Subset of T ;
A46: T | (Cl Hx1) is compact by A45, A6;
Cl Hx1 is sequentially_compact by TOPMETR4:14, A46;
hence STPS /. i is compact by A45, TOPMETR4:15; :: thesis:

end;

then A47: union (rng STPS) is compact by ASCOLI:2;
consider i0 being object such that
A48: i0 in dom STPS by A30, A38, XBOOLE_0:def 1;
reconsider i0 = i0 as Nat by A48;
STPS /. i0 = STPS . i0 by A48, PARTFUN1:def 6;
then STPS /. i0 c= union (rng STPS) by ZFMISC_1:74, A48, FUNCT_1:3;
then reconsider URSTPS = union (rng STPS) as non empty Subset of T by A48, A39;
URSTPS is sequentially_compact by A47, TOPMETR4:15;
then A49: T | URSTPS is compact by TOPMETR4:14;
set MURSTPS = T | URSTPS;
set BM2 = { (Ball (w,((e0 / 2) / 4))) where w is Element of (T | URSTPS) : verum } ;
{ (Ball (w,((e0 / 2) / 4))) where w is Element of (T | URSTPS) : verum } c= bool the carrier of (T | URSTPS)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { (Ball (w,((e0 / 2) / 4))) where w is Element of (T | URSTPS) : verum } ; :: thesis:
then consider x0 being Point of (T | URSTPS) such that
A50: z = Ball (x0,((e0 / 2) / 4)) ;
thus z in bool the carrier of (T | URSTPS) by A50; :: thesis:

end;

then reconsider BM2 = { (Ball (w,((e0 / 2) / 4))) where w is Element of (T | URSTPS) : verum } as Subset-Family of (T | URSTPS) ;
A51: for P being set st P in BM2 holds
ex x0 being Point of (T | URSTPS) ex r being Real st P = Ball (x0,r)

proof

let P be set ; :: thesis:
assume P in BM2 ; :: thesis:
then consider x0 being Point of (T | URSTPS) such that
A52: P = Ball (x0,((e0 / 2) / 4)) ;
take x0 ; :: thesis:
take (e0 / 2) / 4 ; :: thesis:
thus P = Ball (x0,((e0 / 2) / 4)) by A52; :: thesis:

end;

the carrier of (T | URSTPS) c= union BM2

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in the carrier of (T | URSTPS) ; :: thesis:
then reconsider x0 = z as Point of (T | URSTPS) ;
A53: Ball (x0,((e0 / 2) / 4)) in BM2 ;
dist (x0,x0) = 0 by METRIC_1:1;
then x0 in { y where y is Element of (T | URSTPS) : dist (x0,y) < (e0 / 2) / 4 } by A7;
then x0 in Ball (x0,((e0 / 2) / 4)) by METRIC_1:def 14;
hence z in union BM2 by TARSKI:def 4, A53; :: thesis:

end;

then BM2 is Cover of [#] (T | URSTPS) by SETFAM_1:def 11;
then consider BM02 being Subset-Family of (T | URSTPS) such that
A54: ( BM02 c= BM2 & BM02 is Cover of [#] (T | URSTPS) & BM02 is finite ) by A49, TOPMETR:16, A51, TOPMETR:def 4;
reconsider BM02 = BM02 as finite set by A54;
A55: BM02 <> {}

proof

assume BM02 = {} ; :: thesis:
then [#] (T | URSTPS) c= {} by SETFAM_1:def 11, A54, ZFMISC_1:2;
hence contradiction ; :: thesis:

end;

defpred S₃[ object , object ] means ex w being Point of (T | URSTPS) st
( $2 = w & $1 = Ball (w,((e0 / 2) / 4)) );
A56: for D being object st D in BM2 holds
ex w being object st
( w in the carrier of (T | URSTPS) & S₃[D,w] )

proof

let D be object ; :: thesis:
assume D in BM2 ; :: thesis:
then consider w being Element of (T | URSTPS) such that
A57: D = Ball (w,((e0 / 2) / 4)) ;
take w ; :: thesis:
thus ( w in the carrier of (T | URSTPS) & S₃[D,w] ) by A57; :: thesis:

end;

consider U2 being Function of BM2, the carrier of (T | URSTPS) such that
A58: for D being object st D in BM2 holds
S₃[D,U2 . D] from FUNCT_2:sch 1(A56);
A59: for D being object st D in BM2 holds
D = Ball ((U2 /. D),((e0 / 2) / 4))

proof

let D be object ; :: thesis:
assume A60: D in BM2 ; :: thesis:
then A61: ex x0 being Point of (T | URSTPS) st
( U2 . D = x0 & D = Ball (x0,((e0 / 2) / 4)) ) by A58;
dom U2 = BM2 by FUNCT_2:def 1;
hence D = Ball ((U2 /. D),((e0 / 2) / 4)) by A61, A60, PARTFUN1:def 6; :: thesis:

end;

set CF2 = canFS BM02;
A62: len (canFS BM02) = card BM02 by FINSEQ_1:93;
A63: rng (canFS BM02) = BM02 by FUNCT_2:def 3;
A64: dom U2 = BM2 by FUNCT_2:def 1;
then reconsider PS2 = U2 * (canFS BM02) as FinSequence by A63, A54, FINSEQ_1:16;
rng PS2 c= rng U2 by RELAT_1:26;
then reconsider PS2 = PS2 as FinSequence of the carrier of (T | URSTPS) by FINSEQ_1:def 4, XBOOLE_1:1;
A65: dom PS2 = dom (canFS BM02) by A63, A64, A54, RELAT_1:27
.= Seg (card BM02) by A62, FINSEQ_1:def 3 ;
A66: dom (canFS BM02) = Seg (len (canFS BM02)) by FINSEQ_1:def 3
.= dom PS2 by A65, FINSEQ_1:93 ;
A67: for i being Nat st i in dom PS2 holds
(canFS BM02) . i = Ball (((U2 * (canFS BM02)) /. i),((e0 / 2) / 4))

proof

let i be Nat; :: thesis:
assume A68: i in dom PS2 ; :: thesis:
A69: (canFS BM02) . i in rng (canFS BM02) by FUNCT_1:3, A66, A68;
then U2 /. ((canFS BM02) . i) = U2 . ((canFS BM02) . i) by PARTFUN1:def 6, A64, A54
.= PS2 . i by FUNCT_1:12, A68
.= (U2 * (canFS BM02)) /. i by PARTFUN1:def 6, A68 ;
hence (canFS BM02) . i = Ball (((U2 * (canFS BM02)) /. i),((e0 / 2) / 4)) by A69, A59, A54; :: thesis:

end;

union (rng (canFS BM02)) = union BM02 by FUNCT_2:def 3;
then A70: the carrier of (T | URSTPS) c= union (rng (canFS BM02)) by A54, SETFAM_1:def 11;
defpred S₄[ object , object ] means ex sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) st
( $1 = sigm & $2 = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } );
A71: for x being object st x in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) holds
ex B being object st
( B in bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S₄[x,B] )

proof

let x be object ; :: thesis:
assume x in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) ; :: thesis:
then reconsider sigm = x as Function of (Seg (len PS)),(Seg (len (canFS BM02))) by FUNCT_2:66;
set NHx = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } ;
{ f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } c= the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } ; :: thesis:
then ex f being Function of S,T st
( z = f & f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) ;
hence z in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) ; :: thesis:

end;

hence ex B being object st
( B in bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S₄[x,B] ) ; :: thesis:

end;

consider BST being Function of (Funcs ((Seg (len PS)),(Seg (len (canFS BM02))))),(bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H)) such that
A72: for x being object st x in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) holds
S₄[x,BST . x] from FUNCT_2:sch 1(A71);
A73: for sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) holds BST . sigm = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) }

proof

let sigm be Function of (Seg (len PS)),(Seg (len (canFS BM02))); :: thesis:
sigm in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by FUNCT_2:8, A55;
then ex sigm1 being Function of (Seg (len PS)),(Seg (len (canFS BM02))) st
( sigm = sigm1 & BST . sigm = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm1 . i)),((e0 / 2) / 4)) ) ) } ) by A72;
hence BST . sigm = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } ; :: thesis:

end;

A74: Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) c= bool [:(Seg (len PS)),(Seg (len (canFS BM02))):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) ; :: thesis:
then reconsider f = x as Function of (Seg (len PS)),(Seg (len (canFS BM02))) by FUNCT_2:66;
f in bool [:(Seg (len PS)),(Seg (len (canFS BM02))):] ;
hence x in bool [:(Seg (len PS)),(Seg (len (canFS BM02))):] ; :: thesis:

end;

A75: for sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02)))
for f, g being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st f in BST . sigm & g in BST . sigm holds
dist (f,g) < e0

proof

let sigm be Function of (Seg (len PS)),(Seg (len (canFS BM02))); :: thesis:
let f, g be Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H); :: thesis:
assume A76: ( f in BST . sigm & g in BST . sigm ) ; :: thesis:
A77: BST . sigm = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } by A73;
then A78: ex f0 being Function of S,T st
( f = f0 & f0 in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f0 . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) by A76;
then reconsider f0 = f as Function of S,T ;
reconsider f1 = f0 as Function of M,T by A1;
A79: ex f0 being Function of S,T st
( g = f0 & f0 in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f0 . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) by A76, A77;
then reconsider g0 = g as Function of S,T ;
reconsider g1 = g0 as Function of M,T by A1;
A80: for x being Point of S holds dist ((f0 . x),(g0 . x)) <= e0 / 2

proof

let x be Point of S; :: thesis:
x in union (rng (canFS BM0)) by A29;
then consider D being set such that
A81: ( x in D & D in rng (canFS BM0) ) by TARSKI:def 4;
consider i being object such that
A82: ( i in dom (canFS BM0) & D = (canFS BM0) . i ) by A81, FUNCT_1:def 3;
reconsider i = i as Nat by A82;
A83: x in Ball (((U * (canFS BM0)) /. i),d) by A82, A81, A25, A26;
A84: PS /. i = PS . i by A25, A82, PARTFUN1:def 6
.= (U * (canFS BM0)) /. i by A25, A82, PARTFUN1:def 6 ;
reconsider ym = (U * (canFS BM0)) /. i as Point of M ;
reconsider ys = PS /. i as Point of S ;
x in { z where z is Point of M : dist (ym,z) < d } by METRIC_1:def 14, A83;
then A85: ex z being Point of M st
( x = z & dist (ym,z) < d ) ;
then reconsider xm = x as Point of M ;
A86: dist ((f1 . ym),(f1 . xm)) < (e0 / 2) / 4 by A3, A9, A85, A2;
A87: dist ((g1 . ym),(g1 . xm)) < (e0 / 2) / 4 by A3, A9, A85, A2;
i in Seg (len PS) by A25, A82, FINSEQ_1:def 3;
then f0 . ys in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) by A78;
then f0 . ys in { y where y is Element of (T | URSTPS) : dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 } by METRIC_1:def 14;
then A88: ex y being Element of (T | URSTPS) st
( f0 . ys = y & dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 ) ;
then reconsider f0ys = f0 . ys as Point of (T | URSTPS) ;
reconsider u2cf2n = (U2 * (canFS BM02)) /. (sigm . i) as Point of T by TOPMETR:def 1, TARSKI:def 3;
reconsider f0ysm = f0ys as Point of T ;
A90: dist (u2cf2n,(f1 . ym)) < (e0 / 2) / 4 by A84, A88, TOPMETR:def 1;
i in Seg (len PS) by A25, A82, FINSEQ_1:def 3;
then g0 . ys in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) by A79;
then g0 . ys in { y where y is Element of (T | URSTPS) : dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 } by METRIC_1:def 14;
then A91: ex y being Element of (T | URSTPS) st
( g0 . ys = y & dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 ) ;
then reconsider g0ys = g0 . ys as Point of (T | URSTPS) ;
reconsider g0ysm = g0ys as Point of T ;
reconsider g0ysn = g0ysm as Point of T ;
A93: dist (u2cf2n,(g1 . ym)) < (e0 / 2) / 4 by A84, A91, TOPMETR:def 1;
A94: dist (u2cf2n,(f1 . xm)) <= (dist (u2cf2n,(f1 . ym))) + (dist ((f1 . ym),(f1 . xm))) by METRIC_1:4;
(dist (u2cf2n,(f1 . ym))) + (dist ((f1 . ym),(f1 . xm))) < ((e0 / 2) / 4) + ((e0 / 2) / 4) by A86, A90, XREAL_1:8;
then A95: dist (u2cf2n,(f1 . xm)) < (e0 / 2) / 2 by XXREAL_0:2, A94;
A96: dist (u2cf2n,(g1 . xm)) <= (dist (u2cf2n,(g1 . ym))) + (dist ((g1 . ym),(g1 . xm))) by METRIC_1:4;
(dist (u2cf2n,(g1 . ym))) + (dist ((g1 . ym),(g1 . xm))) < ((e0 / 2) / 4) + ((e0 / 2) / 4) by A87, A93, XREAL_1:8;
then A97: dist (u2cf2n,(g1 . xm)) < (e0 / 2) / 2 by XXREAL_0:2, A96;
A98: dist ((f1 . xm),(g1 . xm)) <= (dist (u2cf2n,(f1 . xm))) + (dist (u2cf2n,(g1 . xm))) by METRIC_1:4;
(dist (u2cf2n,(f1 . xm))) + (dist (u2cf2n,(g1 . xm))) < ((e0 / 2) / 2) + ((e0 / 2) / 2) by A95, A97, XREAL_1:8;
hence dist ((f0 . x),(g0 . x)) <= e0 / 2 by XXREAL_0:2, A98; :: thesis:

end;

reconsider f1 = f, g1 = g as Point of (MetricSpace_of_ContinuousFunctions (S,T)) by TOPMETR:def 1, TARSKI:def 3;
dist (f1,g1) <= e0 / 2 by A80, Th12;
then dist (f,g) <= e0 / 2 by TOPMETR:def 1;
hence dist (f,g) < e0 by A8, XXREAL_0:2; :: thesis:

end;

A99: for f being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) ex sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) st f in BST . sigm

proof

let f be Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H); :: thesis:
f in H by A3;
then f in MetricSpace_of_ContinuousFunctions (S,T) ;
then ex g being Function of S,(TopSpaceMetr T) st
( f = g & g is continuous ) ;
then reconsider g = f as Function of the carrier of S, the carrier of T ;
defpred S₅[ object , object ] means ex i, j being Nat st
( i = $1 & j = $2 & g . (PS /. i) in Ball (((U2 * (canFS BM02)) /. j),((e0 / 2) / 4)) );
A100: for x being object st x in Seg (len PS) holds
ex y being object st
( y in Seg (len (canFS BM02)) & S₅[x,y] )

proof

let x be object ; :: thesis:
assume A101: x in Seg (len PS) ; :: thesis:
then reconsider i = x as Nat ;
A102: i in dom PS by A101, FINSEQ_1:def 3;
consider NHx, CHx being non empty Subset of T such that
A103: ( NHx = { (f . (PS /. i)) where f is Function of S,T : f in H } & STPS /. i = Cl NHx ) by A39, A102, A24, A38;
A104: g . (PS /. i) in NHx by A103, A3;
NHx c= Cl NHx by Th1;
then A105: g . (PS /. i) in STPS /. i by A104, A103;
A107: g . (PS /. i) in STPS . i by A105, PARTFUN1:def 6, A102, A24, A38;
STPS . i in rng STPS by A102, A24, A38, FUNCT_1:3;
then g . (PS /. i) in URSTPS by A107, TARSKI:def 4;
then g . (PS /. i) in the carrier of (T | URSTPS) by TOPMETR:def 2;
then consider V being set such that
A108: ( g . (PS /. i) in V & V in rng (canFS BM02) ) by A70, TARSKI:def 4;
consider j being object such that
A109: ( j in dom (canFS BM02) & V = (canFS BM02) . j ) by A108, FUNCT_1:def 3;
A110: j in Seg (card BM02) by A62, FINSEQ_1:def 3, A109;
reconsider j = j as Nat by A109;
A111: (canFS BM02) . j = Ball (((U2 * (canFS BM02)) /. j),((e0 / 2) / 4)) by A67, A65, A110;
j in Seg (len (canFS BM02)) by FINSEQ_1:def 3, A109;
hence ex y being object st
( y in Seg (len (canFS BM02)) & S₅[x,y] ) by A108, A109, A111; :: thesis:

end;

consider sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) such that
A112: for x being object st x in Seg (len PS) holds
S₅[x,sigm . x] from FUNCT_2:sch 1(A100);
A113: for i being Nat st i in Seg (len PS) holds
g . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4))

proof

let i be Nat; :: thesis:
assume i in Seg (len PS) ; :: thesis:
then ex i0, j0 being Nat st
( i0 = i & j0 = sigm . i & g . (PS /. i0) in Ball (((U2 * (canFS BM02)) /. j0),((e0 / 2) / 4)) ) by A112;
hence g . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ; :: thesis:

end;

A114: BST . sigm = { f where f is Function of S,T : ( f in (MetricSpace_of_ContinuousFunctions (S,T)) | H & ( for i being Nat st i in Seg (len PS) holds
f . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ) ) } by A73;
take sigm ; :: thesis:
g in (MetricSpace_of_ContinuousFunctions (S,T)) | H ;
hence f in BST . sigm by A114, A113; :: thesis:

end;

A115: for sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) ex f being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st BST . sigm c= Ball (f,e0)

proof

let sigm be Function of (Seg (len PS)),(Seg (len (canFS BM02))); :: thesis:

per cases ;

suppose A116: BST . sigm = {} ; :: thesis:

take f = the Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H); :: thesis:
thus BST . sigm c= Ball (f,e0) by A116; :: thesis:

end;

suppose BST . sigm <> {} ; :: thesis:

then consider f being object such that
A117: f in BST . sigm by XBOOLE_0:def 1;
sigm in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by A55, FUNCT_2:8;
then A118: BST . sigm in bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) by FUNCT_2:5;
then reconsider f = f as Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) by A117;
take f ; :: thesis:
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A119: z in BST . sigm ; :: thesis:
then reconsider g = z as Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) by A118;
dist (f,g) < e0 by A117, A119, A75;
then g in { y where y is Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) : dist (f,y) < e0 } ;
hence z in Ball (f,e0) by METRIC_1:def 14; :: thesis:

end;

defpred S₅[ object , object ] means ex f being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
( BST . $1 c= Ball (f,e0) & $2 = Ball (f,e0) );
A120: for z being object st z in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) holds
ex f being object st
( f in bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S₅[z,f] )

proof

let z be object ; :: thesis:
assume z in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) ; :: thesis:
then reconsider sigm = z as Function of (Seg (len PS)),(Seg (len (canFS BM02))) by FUNCT_2:66;
ex f being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st BST . sigm c= Ball (f,e0) by A115;
hence ex f being object st
( f in bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S₅[z,f] ) ; :: thesis:

end;

consider FF being Function of (Funcs ((Seg (len PS)),(Seg (len (canFS BM02))))),(bool the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H)) such that
A121: for z being object st z in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) holds
S₅[z,FF . z] from FUNCT_2:sch 1(A120);
A122: dom FF = Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by FUNCT_2:def 1;
reconsider L = rng FF as finite set by A74;
reconsider L = L as Subset-Family of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) ;
take L ; :: thesis:
thus L is finite ; :: thesis:
the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) c= union L

proof

let f be object ; :: according to TARSKI:def 3 :: thesis:
assume f in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) ; :: thesis:
then reconsider g = f as Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) ;
consider sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) such that
A123: g in BST . sigm by A99;
A124: sigm in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by A55, FUNCT_2:8;
then consider w being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that
A125: ( BST . sigm c= Ball (w,e0) & FF . sigm = Ball (w,e0) ) by A121;
FF . sigm in rng FF by FUNCT_1:3, A124, A122;
hence f in union L by TARSKI:def 4, A123, A125; :: thesis:

end;

hence the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) = union L ; :: thesis:
thus for C being Subset of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st C in L holds
ex w being Element of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st C = Ball (w,e0) :: thesis:

proof

let C be Subset of ((MetricSpace_of_ContinuousFunctions (S,T)) | H); :: thesis:
assume C in L ; :: thesis:
then consider x being object such that
A126: ( x in dom FF & C = FF . x ) by FUNCT_1:def 3;
consider w being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that
A127: ( BST . x c= Ball (w,e0) & FF . x = Ball (w,e0) ) by A121, A126;
take w ; :: thesis:
thus C = Ball (w,e0) by A126, A127; :: thesis:

end;

hence (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded ; :: thesis: