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

hereby :: thesis:

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

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

end;

assume A6: ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) ; :: thesis:
for e being Real st e > 0 holds
ex L being Subset-Family of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( L is finite & the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) = union L & ( for C being Subset of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st C in L holds
ex w being Element of ((MetricSpaceNorm (R_NormSpace_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
||.((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
A15: ( 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 A15;
defpred S₁[ object , object ] means ex w being Point of M st
( $2 = w & $1 = Ball (w,d) );
A16: 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
A17: D = Ball (w,d) ;
take w ; :: thesis:
thus ( w in the carrier of M & S₁[D,w] ) by A17; :: thesis:

end;

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

proof

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

end;

set CF = canFS BM0;
A22: len (canFS BM0) = card BM0 by FINSEQ_1:93;
A23: rng (canFS BM0) = BM0 by FUNCT_2:def 3;
A24: dom U = BM by FUNCT_2:def 1;
then reconsider PS = U * (canFS BM0) as FinSequence by A23, A15, 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;
A25: dom PS = dom (canFS BM0) by A23, A24, A15, RELAT_1:27
.= Seg (card BM0) by A22, FINSEQ_1:def 3 ;
A26: dom (canFS BM0) = Seg (len (canFS BM0)) by FINSEQ_1:def 3
.= dom PS by A25, FINSEQ_1:93 ;
A27: 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 A28: i in dom PS ; :: thesis:
then A29: (canFS BM0) . i in rng (canFS BM0) by FUNCT_1:3, A26;
then U /. ((canFS BM0) . i) = U . ((canFS BM0) . i) by PARTFUN1:def 6, A24, A15
.= PS . i by FUNCT_1:12, A28
.= (U * (canFS BM0)) /. i by PARTFUN1:def 6, A28 ;
hence (canFS BM0) . i = Ball (((U * (canFS BM0)) /. i),d) by A29, A19, A15; :: thesis:

end;

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

proof

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

end;

defpred S₂[ object , object ] means ex x being Point of S ex NHx being non empty Subset of T ex CHx being non empty Subset of (MetricSpaceNorm T) st
( $1 = x & NHx = { (f . x) where f is Function of S,T : f in H } & $2 = Cl NHx );
A32: for x being object st x in the carrier of S holds
ex B being object st
( B in bool the carrier of (MetricSpaceNorm 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
A33: f0 in H by XBOOLE_0:def 1;
f0 in R_NormSpace_of_ContinuousFunctions (S,T) by A33;
then ex g being Function of the carrier of S, the carrier of T st
( f0 = g & g is continuous ) ;
then reconsider g = f0 as Function of S,T ;
A34: g . x0 in { (f . x0) where f is Function of S,T : f in H } by A33;
{ (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
A35: ( z = f . x0 & f in H ) ;
thus z in the carrier of T by A35; :: thesis:

end;

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

end;

consider ST being Function of the carrier of S,(bool the carrier of (MetricSpaceNorm T)) such that
A36: for x being object st x in the carrier of S holds
S₂[x,ST . x] from FUNCT_2:sch 1(A32);
A37: dom ST = the carrier of S by FUNCT_2:def 1;
A38: rng PS c= the carrier of S ;
then reconsider STPS = ST * PS as FinSequence by A37, FINSEQ_1:16;
rng STPS c= rng ST by RELAT_1:26;
then reconsider STPS = STPS as FinSequence of bool the carrier of (TopSpaceNorm T) by FINSEQ_1:def 4, XBOOLE_1:1;
A39: dom STPS = Seg (card BM0) by A25, A37, A38, RELAT_1:27;
A40: for i being Nat st i in dom STPS holds
( ex NHx being non empty Subset of T ex CHx being non empty Subset of (MetricSpaceNorm 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 A41: i in dom STPS ; :: thesis:
then A44: STPS /. i = STPS . i by PARTFUN1:def 6
.= ST . (PS . i) by FUNCT_1:12, A41 ;
consider x being Point of S, NHx being non empty Subset of T, CHx being non empty Subset of (MetricSpaceNorm T) such that
A45: ( PS /. i = x & NHx = { (f . x) where f is Function of S,T : f in H } & ST . (PS /. i) = Cl NHx ) by A36;
A46: STPS /. i = Cl NHx by A45, A44, A39, A25, A41, PARTFUN1:def 6;
consider f0 being object such that
A47: f0 in H by XBOOLE_0:def 1;
f0 in R_NormSpace_of_ContinuousFunctions (S,T) by A47;
then ex g being Function of the carrier of S, the carrier of T st
( f0 = g & g is continuous ) ;
then reconsider g = f0 as Function of S,T ;
NHx c= Cl NHx by NORMSP_3:4;
hence ( ex NHx being non empty Subset of T ex CHx being non empty Subset of (MetricSpaceNorm 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 A45, A46; :: 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 being non empty Subset of T, CHx being non empty Subset of (MetricSpaceNorm T) such that
A48: ( NHx = { (f . (PS /. i)) where f is Function of S,T : f in H } & STPS /. i = Cl NHx ) by A40;
reconsider Hx1 = NHx as non empty Subset of (MetricSpaceNorm T) ;
A49: (MetricSpaceNorm T) | (Cl Hx1) is compact by A48, A6;
reconsider NHx1 = Hx1 as non empty Subset of T ;
NHx1 c= Cl NHx1 by NORMSP_3:4;
then reconsider KK = Cl NHx1 as non empty Subset of (TopSpaceNorm T) ;
A50: Cl NHx1 = Cl Hx1 by Th1;
consider RNS being RealNormSpace such that
A51: ( RNS = NORMSTR(# the carrier of T, the ZeroF of T, the U5 of T, the U7 of T, the normF of T #) & the topology of T = the topology of (TopSpaceNorm RNS) ) by C0SP3:def 6;
A52: MetricSpaceNorm RNS = MetricSpaceNorm T by Th15, A51;
reconsider RNV1 = Cl NHx1 as Subset of RNS by A51;
A53: TopSpaceNorm T = TopSpaceNorm RNS by Th15, A51;
Cl Hx1 is sequentially_compact by TOPMETR4:14, A49;
then RNV1 is compact by A52, TOPMETR4:18, A50;
hence STPS /. i is compact by A48, TOPMETR4:19, A53; :: thesis:

end;

then A54: union (rng STPS) is compact by Th2;
consider i0 being object such that
A55: i0 in dom STPS by A31, A39, XBOOLE_0:def 1;
reconsider i0 = i0 as Nat by A55;
STPS /. i0 = STPS . i0 by A55, PARTFUN1:def 6;
then STPS /. i0 c= union (rng STPS) by ZFMISC_1:74, A55, FUNCT_1:3;
then reconsider URSTPS = union (rng STPS) as non empty Subset of (MetricSpaceNorm T) by A55, A40;
URSTPS is sequentially_compact by A54, TOPMETR4:15;
then A58: (MetricSpaceNorm T) | URSTPS is compact by TOPMETR4:14;
set MURSTPS = (MetricSpaceNorm T) | URSTPS;
set BM2 = { (Ball (w,((e0 / 2) / 4))) where w is Element of ((MetricSpaceNorm T) | URSTPS) : verum } ;
{ (Ball (w,((e0 / 2) / 4))) where w is Element of ((MetricSpaceNorm T) | URSTPS) : verum } c= bool the carrier of ((MetricSpaceNorm 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 ((MetricSpaceNorm T) | URSTPS) : verum } ; :: thesis:
then consider x0 being Point of ((MetricSpaceNorm T) | URSTPS) such that
A59: z = Ball (x0,((e0 / 2) / 4)) ;
thus z in bool the carrier of ((MetricSpaceNorm T) | URSTPS) by A59; :: thesis:

end;

then reconsider BM2 = { (Ball (w,((e0 / 2) / 4))) where w is Element of ((MetricSpaceNorm T) | URSTPS) : verum } as Subset-Family of ((MetricSpaceNorm T) | URSTPS) ;
A60: for P being set st P in BM2 holds
ex x0 being Point of ((MetricSpaceNorm 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 ((MetricSpaceNorm T) | URSTPS) such that
A61: P = Ball (x0,((e0 / 2) / 4)) ;
take x0 ; :: thesis:
take (e0 / 2) / 4 ; :: thesis:
thus P = Ball (x0,((e0 / 2) / 4)) by A61; :: thesis:

end;

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in the carrier of ((MetricSpaceNorm T) | URSTPS) ; :: thesis:
then reconsider x0 = z as Point of ((MetricSpaceNorm T) | URSTPS) ;
A62: Ball (x0,((e0 / 2) / 4)) in BM2 ;
dist (x0,x0) = 0 by METRIC_1:1;
then x0 in { y where y is Element of ((MetricSpaceNorm 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, A62; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

set CF2 = canFS BM02;
A72: len (canFS BM02) = card BM02 by FINSEQ_1:93;
A73: rng (canFS BM02) = BM02 by FUNCT_2:def 3;
A74: dom U2 = BM2 by FUNCT_2:def 1;
then reconsider PS2 = U2 * (canFS BM02) as FinSequence by A73, A64, FINSEQ_1:16;
rng PS2 c= rng U2 by RELAT_1:26;
then reconsider PS2 = PS2 as FinSequence of the carrier of ((MetricSpaceNorm T) | URSTPS) by FINSEQ_1:def 4, XBOOLE_1:1;
A75: dom PS2 = dom (canFS BM02) by A73, A74, A64, RELAT_1:27
.= Seg (card BM02) by A72, FINSEQ_1:def 3 ;
A76: dom (canFS BM02) = Seg (len (canFS BM02)) by FINSEQ_1:def 3
.= dom PS2 by A75, FINSEQ_1:93 ;
A77: 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 A78: i in dom PS2 ; :: thesis:
A79: (canFS BM02) . i in rng (canFS BM02) by FUNCT_1:3, A76, A78;
then U2 /. ((canFS BM02) . i) = U2 . ((canFS BM02) . i) by PARTFUN1:def 6, A74, A64
.= PS2 . i by FUNCT_1:12, A78
.= (U2 * (canFS BM02)) /. i by PARTFUN1:def 6, A78 ;
hence (canFS BM02) . i = Ball (((U2 * (canFS BM02)) /. i),((e0 / 2) / 4)) by A79, A69, A64; :: thesis:

end;

union (rng (canFS BM02)) = union BM02 by FUNCT_2:def 3;
then A80: the carrier of ((MetricSpaceNorm T) | URSTPS) c= union (rng (canFS BM02)) by A64, 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 (MetricSpaceNorm (R_NormSpace_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)) ) ) } );
A81: 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 ((MetricSpaceNorm (R_NormSpace_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 (MetricSpaceNorm (R_NormSpace_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 (MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_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 (MetricSpaceNorm (R_NormSpace_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 (MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ; :: thesis:

end;

hence ex B being object st
( B in bool the carrier of ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H)) such that
A82: 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(A81);
A83: 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 (MetricSpaceNorm (R_NormSpace_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, A65;
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 (MetricSpaceNorm (R_NormSpace_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 A82;
hence BST . sigm = { f where f is Function of S,T : ( f in (MetricSpaceNorm (R_NormSpace_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;

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

A85: for sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02)))
for f, g being Point of ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H); :: thesis:
assume A86: ( f in BST . sigm & g in BST . sigm ) ; :: thesis:
A87: BST . sigm = { f where f is Function of S,T : ( f in (MetricSpaceNorm (R_NormSpace_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 A83;
then A88: ex f0 being Function of S,T st
( f = f0 & f0 in (MetricSpaceNorm (R_NormSpace_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 A86;
then reconsider f0 = f as Function of S,T ;
reconsider f1 = f0 as Function of M,T by A1;
A89: ex f0 being Function of S,T st
( g = f0 & f0 in (MetricSpaceNorm (R_NormSpace_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 A86, A87;
then reconsider g0 = g as Function of S,T ;
reconsider g1 = g0 as Function of M,T by A1;
A90: for x being Point of S holds ||.((f0 . x) - (g0 . x)).|| <= e0 / 2

proof

let x be Point of S; :: thesis:
x in union (rng (canFS BM0)) by A30;
then consider D being set such that
A91: ( x in D & D in rng (canFS BM0) ) by TARSKI:def 4;
consider i being object such that
A92: ( i in dom (canFS BM0) & D = (canFS BM0) . i ) by A91, FUNCT_1:def 3;
reconsider i = i as Nat by A92;
A93: x in Ball (((U * (canFS BM0)) /. i),d) by A92, A91, A26, A27;
A94: PS /. i = PS . i by A26, A92, PARTFUN1:def 6
.= (U * (canFS BM0)) /. i by A26, A92, 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, A93;
then A95: ex z being Point of M st
( x = z & dist (ym,z) < d ) ;
then reconsider xm = x as Point of M ;
A96: ||.((f1 . ym) - (f1 . xm)).|| < (e0 / 2) / 4 by A3, A9, A95, A2;
A97: ||.((g1 . ym) - (g1 . xm)).|| < (e0 / 2) / 4 by A3, A9, A95, A2;
i in Seg (len PS) by A26, A92, FINSEQ_1:def 3;
then f0 . ys in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) by A88;
then f0 . ys in { y where y is Element of ((MetricSpaceNorm T) | URSTPS) : dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 } by METRIC_1:def 14;
then A98: ex y being Element of ((MetricSpaceNorm T) | URSTPS) st
( f0 . ys = y & dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 ) ;
then reconsider f0ys = f0 . ys as Point of ((MetricSpaceNorm T) | URSTPS) ;
reconsider u2cf2 = (U2 * (canFS BM02)) /. (sigm . i) as Point of (MetricSpaceNorm T) by TOPMETR:def 1, TARSKI:def 3;
reconsider f0ysm = f0ys as Point of (MetricSpaceNorm T) ;
A99: dist (u2cf2,f0ysm) < (e0 / 2) / 4 by A98, TOPMETR:def 1;
reconsider u2cf2n = u2cf2, f0ysn = f0ysm as Point of T ;
A100: ||.(u2cf2n - (f1 . ym)).|| < (e0 / 2) / 4 by A94, A99, NORMSP_2:def 1;
i in Seg (len PS) by A26, A92, FINSEQ_1:def 3;
then g0 . ys in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) by A89;
then g0 . ys in { y where y is Element of ((MetricSpaceNorm T) | URSTPS) : dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 } by METRIC_1:def 14;
then A101: ex y being Element of ((MetricSpaceNorm T) | URSTPS) st
( g0 . ys = y & dist (((U2 * (canFS BM02)) /. (sigm . i)),y) < (e0 / 2) / 4 ) ;
then reconsider g0ys = g0 . ys as Point of ((MetricSpaceNorm T) | URSTPS) ;
reconsider g0ysm = g0ys as Point of (MetricSpaceNorm T) ;
A102: dist (u2cf2,g0ysm) < (e0 / 2) / 4 by A101, TOPMETR:def 1;
reconsider g0ysn = g0ysm as Point of T ;
A103: ||.(u2cf2n - (g1 . ym)).|| < (e0 / 2) / 4 by A94, A102, NORMSP_2:def 1;
u2cf2n - (f1 . xm) = ((u2cf2n - (f1 . ym)) + (f1 . ym)) - (f1 . xm) by RLVECT_4:1
.= (u2cf2n - (f1 . ym)) + ((f1 . ym) - (f1 . xm)) by RLVECT_1:28 ;
then A104: ||.(u2cf2n - (f1 . xm)).|| <= ||.(u2cf2n - (f1 . ym)).|| + ||.((f1 . ym) - (f1 . xm)).|| by NORMSP_1:def 1;
||.(u2cf2n - (f1 . ym)).|| + ||.((f1 . ym) - (f1 . xm)).|| < ((e0 / 2) / 4) + ((e0 / 2) / 4) by A96, A100, XREAL_1:8;
then A105: ||.(u2cf2n - (f1 . xm)).|| < (e0 / 2) / 2 by XXREAL_0:2, A104;
u2cf2n - (g1 . xm) = ((u2cf2n - (g1 . ym)) + (g1 . ym)) - (g1 . xm) by RLVECT_4:1
.= (u2cf2n - (g1 . ym)) + ((g1 . ym) - (g1 . xm)) by RLVECT_1:28 ;
then A106: ||.(u2cf2n - (g1 . xm)).|| <= ||.(u2cf2n - (g1 . ym)).|| + ||.((g1 . ym) - (g1 . xm)).|| by NORMSP_1:def 1;
||.(u2cf2n - (g1 . ym)).|| + ||.((g1 . ym) - (g1 . xm)).|| < ((e0 / 2) / 4) + ((e0 / 2) / 4) by A97, A103, XREAL_1:8;
then A107: ||.(u2cf2n - (g1 . xm)).|| < (e0 / 2) / 2 by XXREAL_0:2, A106;
(f1 . xm) - (g1 . xm) = (((f1 . xm) - u2cf2n) + u2cf2n) - (g1 . xm) by RLVECT_4:1
.= ((f1 . xm) - u2cf2n) + (u2cf2n - (g1 . xm)) by RLVECT_1:28 ;
then ||.((f1 . xm) - (g1 . xm)).|| <= ||.((f1 . xm) - u2cf2n).|| + ||.(u2cf2n - (g1 . xm)).|| by NORMSP_1:def 1;
then A108: ||.((f1 . xm) - (g1 . xm)).|| <= ||.(u2cf2n - (f1 . xm)).|| + ||.(u2cf2n - (g1 . xm)).|| by NORMSP_1:7;
||.(u2cf2n - (f1 . xm)).|| + ||.(u2cf2n - (g1 . xm)).|| < ((e0 / 2) / 2) + ((e0 / 2) / 2) by A105, A107, XREAL_1:8;
hence ||.((f0 . x) - (g0 . x)).|| <= e0 / 2 by XXREAL_0:2, A108; :: thesis:

end;

reconsider f1 = f, g1 = g as Point of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) by TOPMETR:def 1, TARSKI:def 3;
reconsider f2 = f1, g2 = g1 as Point of (R_NormSpace_of_ContinuousFunctions (S,T)) ;
A109: ( f2 in BoundedFunctions ( the carrier of S,T) & g2 in BoundedFunctions ( the carrier of S,T) ) by C0SP3:34;
reconsider f3 = f2, g3 = g2 as Point of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by C0SP3:34;
reconsider f4 = f2, g4 = g2 as bounded Function of the carrier of S,T by RSSPACE4:def 5, A109;
reconsider fg4 = f3 - g3 as bounded Function of the carrier of S,T by RSSPACE4:def 5;
A110: ||.(f3 - g3).|| = upper_bound (PreNorms fg4) by RSSPACE4:14;
for s being Real st s in PreNorms fg4 holds
s <= e0 / 2

proof

let s be Real; :: thesis:
assume s in PreNorms fg4 ; :: thesis:
then consider t being Element of S such that
A111: s = ||.(fg4 . t).|| ;
fg4 . t = (f4 . t) - (g4 . t) by RSSPACE4:24
.= (f0 . t) - (g0 . t) ;
hence s <= e0 / 2 by A90, A111; :: thesis:

end;

then A112: ||.(f3 - g3).|| <= e0 / 2 by A110, SEQ_4:45;
A113: (- 1) * g2 = (- 1) * g3 by C0SP3:39;
f2 - g2 = f2 + ((- 1) * g2) by RLVECT_1:16
.= f3 + ((- 1) * g3) by C0SP3:38, A113
.= f3 - g3 by RLVECT_1:16 ;
then ||.(f2 - g2).|| <= e0 / 2 by A112, C0SP3:36;
then dist (f1,g1) <= e0 / 2 by NORMSP_2:def 1;
then dist (f,g) <= e0 / 2 by TOPMETR:def 1;
hence dist (f,g) < e0 by A8, XXREAL_0:2; :: thesis:

end;

A114: for f being Point of ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H); :: thesis:
f in H by A3;
then f in R_NormSpace_of_ContinuousFunctions (S,T) ;
then ex g being Function of the carrier of S, the carrier of 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)) );
A115: 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 A116: x in Seg (len PS) ; :: thesis:
then reconsider i = x as Nat ;
A117: i in dom PS by A116, FINSEQ_1:def 3;
consider NHx being non empty Subset of T, CHx being non empty Subset of (MetricSpaceNorm T) such that
A119: ( NHx = { (f . (PS /. i)) where f is Function of S,T : f in H } & STPS /. i = Cl NHx ) by A40, A117, A25, A39;
A120: g . (PS /. i) in NHx by A119, A3;
NHx c= Cl NHx by NORMSP_3:4;
then A121: g . (PS /. i) in STPS /. i by A120, A119;
A122: i in dom STPS by A117, A25, A39;
A123: g . (PS /. i) in STPS . i by A121, PARTFUN1:def 6, A117, A25, A39;
STPS . i in rng STPS by A122, FUNCT_1:3;
then g . (PS /. i) in URSTPS by A123, TARSKI:def 4;
then g . (PS /. i) in the carrier of ((MetricSpaceNorm T) | URSTPS) by TOPMETR:def 2;
then consider V being set such that
A124: ( g . (PS /. i) in V & V in rng (canFS BM02) ) by A80, TARSKI:def 4;
consider j being object such that
A125: ( j in dom (canFS BM02) & V = (canFS BM02) . j ) by A124, FUNCT_1:def 3;
A126: j in Seg (card BM02) by A72, FINSEQ_1:def 3, A125;
reconsider j = j as Nat by A125;
A127: (canFS BM02) . j = Ball (((U2 * (canFS BM02)) /. j),((e0 / 2) / 4)) by A77, A75, A126;
j in Seg (len (canFS BM02)) by FINSEQ_1:def 3, A125;
hence ex y being object st
( y in Seg (len (canFS BM02)) & S₅[x,y] ) by A124, A125, A127; :: thesis:

end;

consider sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) such that
A128: for x being object st x in Seg (len PS) holds
S₅[x,sigm . x] from FUNCT_2:sch 1(A115);
A129: 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 A128;
hence g . (PS /. i) in Ball (((U2 * (canFS BM02)) /. (sigm . i)),((e0 / 2) / 4)) ; :: thesis:

end;

A130: BST . sigm = { f where f is Function of S,T : ( f in (MetricSpaceNorm (R_NormSpace_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 A83;
take sigm ; :: thesis:
g in (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H ;
hence f in BST . sigm by A130, A129; :: thesis:

end;

A131: for sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) ex f being Point of ((MetricSpaceNorm (R_NormSpace_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 A132: BST . sigm = {} ; :: thesis:

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

end;

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

then consider f being object such that
A133: f in BST . sigm by XBOOLE_0:def 1;
sigm in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by A65, FUNCT_2:8;
then A134: BST . sigm in bool the carrier of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by FUNCT_2:5;
then reconsider f = f as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A133;
take f ; :: thesis:
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A135: z in BST . sigm ; :: thesis:
then reconsider g = z as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) by A134;
dist (f,g) < e0 by A133, A135, A85;
then g in { y where y is Point of ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st
( BST . $1 c= Ball (f,e0) & $2 = Ball (f,e0) );
A136: 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 ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) st BST . sigm c= Ball (f,e0) by A131;
hence ex f being object st
( f in bool the carrier of ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H)) such that
A138: 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(A136);
A139: dom FF = Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by FUNCT_2:def 1;
reconsider L = rng FF as finite set by A84;
reconsider L = L as Subset-Family of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
take L ; :: thesis:
thus L is finite ; :: thesis:
the carrier of ((MetricSpaceNorm (R_NormSpace_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 ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ; :: thesis:
then reconsider g = f as Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) ;
consider sigm being Function of (Seg (len PS)),(Seg (len (canFS BM02))) such that
A140: g in BST . sigm by A114;
A141: sigm in Funcs ((Seg (len PS)),(Seg (len (canFS BM02)))) by A65, FUNCT_2:8;
then consider w being Point of ((MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H) such that
A142: ( BST . sigm c= Ball (w,e0) & FF . sigm = Ball (w,e0) ) by A138;
FF . sigm in rng FF by FUNCT_1:3, A141, A139;
hence f in union L by TARSKI:def 4, A140, A142; :: thesis:

end;

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

proof

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

end;

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