let M be non empty MetrSpace; :: thesis:
let S be non empty compact TopSpace; :: thesis:
let T be NormedLinearTopSpace; :: thesis:
assume that
A1: S = TopSpaceMetr M and
A2: T is complete and
A3: ( T is finite-dimensional & dim T <> 0 ) ; :: 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 A4: G = H ; :: thesis:
hence ( (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded implies ( G is equibounded & G is equicontinuous ) ) by A1, A2, ASCOLI:13; :: thesis:
assume A5: ( G is equibounded & G is equicontinuous ) ; :: thesis:
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

proof

let x be Point of S; :: thesis:
let Hx be non empty Subset of (MetricSpaceNorm T); :: thesis:
assume A6: Hx = { (f . x) where f is Function of S,T : f in H } ; :: thesis:
reconsider Tx = Hx as non empty Subset of (TopSpaceNorm T) ;
reconsider Fx = Hx as non empty Subset of T ;
A7: Cl Fx = Cl Hx by ASCOLI:1;
consider RNS being RealNormSpace such that
A8: ( RNS = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & the topology of T = the topology of (TopSpaceNorm RNS) ) by C0SP3:def 6;
A9: ( RNS is finite-dimensional & dim RNS <> 0 ) by A3, A8, Th25;
reconsider Fx0 = Fx as non empty Subset of RNS by A8;
A10: for a, b being Element of RNS holds (distance_by_norm_of RNS) . (a,b) = (distance_by_norm_of T) . (a,b)

proof

let a, b be Element of RNS; :: thesis:
reconsider a1 = a, b1 = b as Element of T by A8;
A11: a - b = a + ((- 1) * b) by RLVECT_1:16
.= the addF of T . (a1,((- 1) * b1)) by A8
.= a1 - b1 by RLVECT_1:16 ;
thus (distance_by_norm_of RNS) . (a,b) = ||.(a - b).|| by NORMSP_2:def 1
.= ||.(a1 - b1).|| by A11, A8
.= (distance_by_norm_of T) . (a,b) by NORMSP_2:def 1 ; :: thesis:

end;

A12: MetricSpaceNorm RNS = MetricSpaceNorm T by A10, A8, BINOP_1:2;
then A13: Cl Fx0 = Cl Fx by A7, ASCOLI:1;
reconsider ClHx = Cl Hx as non empty Subset of (MetricSpaceNorm RNS) by A8;
consider K being Real such that
A14: for f being Function of the carrier of M, the carrier of T st f in G holds
for x being Element of M holds ||.(f . x).|| <= K by A5;
reconsider x0 = x as Element of M by A1;

A15: now :: thesis:

let y be Point of RNS; :: thesis:
assume y in Fx0 ; :: thesis:
then consider f being Function of S,T such that
A16: ( y = f . x & f in H ) by A6;
reconsider g = f as Function of the carrier of M, the carrier of T by A1;
||.(g . x0).|| = ||.y.|| by A16, A8;
hence ||.y.|| <= K by A4, A14, A16; :: thesis:

end;

set r = K + 1;
for y being Point of RNS st y in Cl Fx0 holds
||.y.|| < K + 1

proof

let y be Point of RNS; :: thesis:
assume y in Cl Fx0 ; :: thesis:
then consider seq being sequence of RNS such that
A17: ( rng seq c= Fx0 & seq is convergent & lim seq = y ) by NORMSP_3:6;
A18: { y where y is Point of RNS : ||.((0. RNS) - y).|| <= K } is closed Subset of (TopSpaceNorm RNS) by NORMSP_2:9;
then reconsider B = { y where y is Point of RNS : ||.((0. RNS) - y).|| <= K } as Subset of RNS ;
A19: B is closed by NORMSP_2:15, A18;
rng seq c= B

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A20: z in rng seq ; :: thesis:
then reconsider z1 = z as Point of RNS ;
||.z1.|| <= K by A15, A17, A20;
then ||.((0. RNS) - z1).|| <= K by NORMSP_1:2;
hence z in B ; :: thesis:

end;

then y in B by A17, A19;
then ex z being Point of RNS st
( y = z & ||.((0. RNS) - z).|| <= K ) ;
then A21: ||.y.|| <= K by NORMSP_1:2;
K + 0 < 1 + K by XREAL_1:8;
hence ||.y.|| < K + 1 by A21, XXREAL_0:2; :: thesis:

end;

then Cl Fx0 is compact by A9, REAL_NS3:38;
then ClHx is sequentially_compact by A7, A13, TOPMETR4:18;
hence (MetricSpaceNorm T) | (Cl Hx) is compact by A12, TOPMETR4:14; :: thesis:

end;

hence (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded by A1, A2, A4, A5, ASCOLI:16; :: thesis: