let RNS be RealNormSpace; :: thesis:
let T be NormedLinearTopSpace; :: thesis:
let X be non empty Subset of RNS; :: thesis:
let S be non empty strict compact TopSpace; :: thesis:
let G be non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis:
assume that
A1: S is SubSpace of TopSpaceNorm RNS and
A2: the carrier of S = X and
X is compact and
A3: ( T is complete & T is finite-dimensional & dim T <> 0 ) and
A4: ex K, D being Real st
( 0 < K & 0 < D & ( for F being Function of X,T st F in G holds
( ( for x, y being Point of RNS st x in X & y in X holds
||.((F /. x) - (F /. y)).|| <= D * ||.(x - y).|| ) & ( for x being Point of RNS st x in X holds
||.(F /. x).|| <= K ) ) ) ) ; :: thesis:
reconsider Y = X as non empty Subset of (MetricSpaceNorm RNS) ;
reconsider M = (MetricSpaceNorm RNS) | Y as non empty MetrSpace ;
A5: ( [#] S c= [#] (TopSpaceNorm RNS) & ( for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of (TopSpaceNorm RNS) st
( Q in the topology of (TopSpaceNorm RNS) & P = Q /\ ([#] S) ) ) ) ) by A1, PRE_TOPC:def 4;
A6: the carrier of M = Y by TOPMETR:def 2;
A7: for z being object holds
( z in the topology of S iff z in Family_open_set M )

let z be object ; :: thesis:

hereby :: thesis:

assume A8: z in the topology of S ; :: thesis:
then reconsider P = z as Subset of S ;
consider Q being Subset of (TopSpaceNorm RNS) such that
A9: ( Q in the topology of (TopSpaceNorm RNS) & P = Q /\ ([#] S) ) by A1, PRE_TOPC:def 4, A8;
reconsider P1 = P as Subset of M by A2, TOPMETR:def 2;
for x being Element of M st x in P1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= P1 )

proof

let x be Element of M; :: thesis:
assume x in P1 ; :: thesis:
then A10: ( x in Q & x in [#] S ) by A9, XBOOLE_0:def 4;
reconsider x1 = x as Point of (MetricSpaceNorm RNS) by TOPMETR:8;
consider r being Real such that
A11: ( r > 0 & Ball (x1,r) c= Q ) by A9, A10, PCOMPS_1:def 4;
take r ; :: thesis:
thus r > 0 by A11; :: thesis:
Ball (x,r) = (Ball (x1,r)) /\ the carrier of M by TOPMETR:9
.= (Ball (x1,r)) /\ ([#] S) by A2, TOPMETR:def 2 ;
hence Ball (x,r) c= P1 by A9, A11, XBOOLE_1:27; :: thesis:

end;

hence z in Family_open_set M by PCOMPS_1:def 4; :: thesis:

end;

assume A13: z in Family_open_set M ; :: thesis:
then reconsider P1 = z as Subset of M ;
reconsider P = P1 as Subset of S by A2, TOPMETR:def 2;
defpred S₁[ object , object ] means ex x being Point of M ex r being Real st
( $1 = x & $2 = r & 0 < r & Ball (x,r) c= P1 );
A14: for z being object st z in P1 holds
ex r being object st
( r in REAL & S₁[z,r] )

proof

let z be object ; :: thesis:
assume A15: z in P1 ; :: thesis:
then reconsider x = z as Point of M ;
consider r being Real such that
A16: ( r > 0 & Ball (x,r) c= P1 ) by A13, A15, PCOMPS_1:def 4;
thus ex r being object st
( r in REAL & S₁[z,r] ) by A16, XREAL_0:def 1; :: thesis:

end;

consider R being Function of P1,REAL such that
A17: for z being object st z in P1 holds
S₁[z,R . z] from FUNCT_2:sch 1(A14);
A18: for z being Point of M st z in P1 holds
( Ball (z,(R . z)) c= P1 & 0 < R . z )

proof

let z be Point of M; :: thesis:
assume z in P1 ; :: thesis:
then S₁[z,R . z] by A17;
hence ( Ball (z,(R . z)) c= P1 & 0 < R . z ) ; :: thesis:

end;

set B = { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } ;
set Q = union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } ;
A19: for z being object st z in union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } holds
ex x1 being Point of (MetricSpaceNorm RNS) st
( z in Ball (x1,(R /. x1)) & Ball (x1,(R /. x1)) c= union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } & 0 < R /. x1 & ex x being Point of M st
( x = x1 & x in P1 & Ball (x,(R /. x1)) c= P1 ) )

proof

let z be object ; :: thesis:
assume z in union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } ; :: thesis:
then consider X being set such that
A20: ( z in X & X in { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } ) by TARSKI:def 4;
consider x1 being Point of (MetricSpaceNorm RNS) such that
A21: ( X = Ball (x1,(R /. x1)) & ex x being Point of M st
( x = x1 & x in P1 ) ) by A20;
take x1 ; :: thesis:
consider x being Point of M such that
A22: ( x = x1 & x in P1 ) by A21;
A23: ( Ball (x,(R . x)) c= P1 & 0 < R . x ) by A18, A22;
dom R = P1 by FUNCT_2:def 1;
then R . x = R /. x1 by A22, PARTFUN1:def 6;
hence ( z in Ball (x1,(R /. x1)) & Ball (x1,(R /. x1)) c= union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } & 0 < R /. x1 & ex x being Point of M st
( x = x1 & x in P1 & Ball (x,(R /. x1)) c= P1 ) ) by A20, A21, A22, A23, ZFMISC_1:74; :: thesis:

end;

for z being object st z in union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } holds
z in the carrier of (TopSpaceNorm RNS)

proof

let z be object ; :: thesis:
assume z in union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } ; :: thesis:
then consider x1 being Point of (MetricSpaceNorm RNS) such that
A24: ( z in Ball (x1,(R /. x1)) & Ball (x1,(R /. x1)) c= union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } & 0 < R /. x1 & ex x being Point of M st
( x = x1 & x in P1 & Ball (x,(R /. x1)) c= P1 ) ) by A19;
thus z in the carrier of (TopSpaceNorm RNS) by A24; :: thesis:

end;

then union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } c= the carrier of (TopSpaceNorm RNS) ;
then reconsider Q = union { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } as Subset of (TopSpaceNorm RNS) ;
for x being Element of (MetricSpaceNorm RNS) st x in Q holds
ex r being Real st
( r > 0 & Ball (x,r) c= Q )

proof

let x be Element of (MetricSpaceNorm RNS); :: thesis:
assume x in Q ; :: thesis:
then consider x1 being Point of (MetricSpaceNorm RNS) such that
A25: ( x in Ball (x1,(R /. x1)) & Ball (x1,(R /. x1)) c= Q & 0 < R /. x1 & ex x being Point of M st
( x = x1 & x in P1 & Ball (x,(R /. x1)) c= P1 ) ) by A19;
x in { y where y is Element of (MetricSpaceNorm RNS) : dist (x1,y) < R /. x1 } by METRIC_1:def 14, A25;
then ex y being Element of (MetricSpaceNorm RNS) st
( x = y & dist (x1,y) < R /. x1 ) ;
then A26: 0 < (R /. x1) - (dist (x1,x)) by XREAL_1:50;
set r = ((R /. x1) - (dist (x1,x))) / 2;
take ((R /. x1) - (dist (x1,x))) / 2 ; :: thesis:
thus 0 < ((R /. x1) - (dist (x1,x))) / 2 by A26, XREAL_1:215; :: thesis:
A27: ((R /. x1) - (dist (x1,x))) / 2 < (R /. x1) - (dist (x1,x)) by A26, XREAL_1:216;
for z being object st z in Ball (x,(((R /. x1) - (dist (x1,x))) / 2)) holds
z in Ball (x1,(R /. x1))

proof

let z be object ; :: thesis:
assume A28: z in Ball (x,(((R /. x1) - (dist (x1,x))) / 2)) ; :: thesis:
then reconsider w = z as Point of (MetricSpaceNorm RNS) ;
w in { y where y is Element of (MetricSpaceNorm RNS) : dist (x,y) < ((R /. x1) - (dist (x1,x))) / 2 } by METRIC_1:def 14, A28;
then A29: ex y being Element of (MetricSpaceNorm RNS) st
( w = y & dist (x,y) < ((R /. x1) - (dist (x1,x))) / 2 ) ;
A30: dist (x1,w) <= (dist (x1,x)) + (dist (x,w)) by METRIC_1:4;
A31: (dist (x1,x)) + (dist (x,w)) < (dist (x1,x)) + (((R /. x1) - (dist (x1,x))) / 2) by A29, XREAL_1:8;
(dist (x1,x)) + (((R /. x1) - (dist (x1,x))) / 2) < (dist (x1,x)) + ((R /. x1) - (dist (x1,x))) by A27, XREAL_1:8;
then (dist (x1,x)) + (dist (x,w)) < R /. x1 by A31, XXREAL_0:2;
then dist (x1,w) < R /. x1 by A30, XXREAL_0:2;
then w in { y where y is Element of (MetricSpaceNorm RNS) : dist (x1,y) < R /. x1 } ;
hence z in Ball (x1,(R /. x1)) by METRIC_1:def 14; :: thesis:

end;

hence Ball (x,(((R /. x1) - (dist (x1,x))) / 2)) c= Q by A25; :: thesis:

end;

then A32: Q in the topology of (TopSpaceNorm RNS) by PCOMPS_1:def 4;
for z being object holds
( z in P iff z in Q /\ ([#] S) )

proof

let z be object ; :: thesis:

hereby :: thesis:

assume A33: z in P ; :: thesis:
then reconsider w = z as Point of M ;
A34: ( Ball (w,(R . w)) c= P1 & 0 < R . w ) by A18, A33;
reconsider w1 = w as Point of (MetricSpaceNorm RNS) by TARSKI:def 3, A6;
A35: Ball (w,(R . w)) = (Ball (w1,(R . w))) /\ the carrier of M by TOPMETR:9
.= (Ball (w1,(R . w))) /\ ([#] S) by A2, TOPMETR:def 2 ;
dist (w,w) < R . w by A34, METRIC_1:1;
then w in { y where y is Element of M : dist (w,y) < R . w } ;
then A36: w in Ball (w,(R . w)) by METRIC_1:def 14;
dom R = P1 by FUNCT_2:def 1;
then R . w = R /. w1 by A33, PARTFUN1:def 6;
then Ball (w1,(R . w)) in { (Ball (x1,(R /. x1))) where x1 is Point of (MetricSpaceNorm RNS) : ex x being Point of M st
( x = x1 & x in P1 ) } by A33;
then Ball (w1,(R . w)) c= Q by ZFMISC_1:74;
then (Ball (w1,(R . w))) /\ ([#] S) c= Q /\ ([#] S) by XBOOLE_1:27;
hence z in Q /\ ([#] S) by A36, A35; :: thesis:

end;

assume A37: z in Q /\ ([#] S) ; :: thesis:
then ( z in Q & z in [#] S ) by XBOOLE_0:def 4;
then consider x1 being Point of (MetricSpaceNorm RNS) such that
A38: ( z in Ball (x1,(R /. x1)) & Ball (x1,(R /. x1)) c= Q & 0 < R /. x1 & ex x being Point of M st
( x = x1 & x in P1 & Ball (x,(R /. x1)) c= P1 ) ) by A19;
consider x being Point of M such that
A39: ( x = x1 & x in P1 & Ball (x,(R /. x1)) c= P1 ) by A38;
Ball (x,(R /. x1)) = (Ball (x1,(R /. x1))) /\ the carrier of M by TOPMETR:9, A39
.= (Ball (x1,(R /. x1))) /\ ([#] S) by A2, TOPMETR:def 2 ;
then z in Ball (x,(R /. x1)) by A37, A38, XBOOLE_0:def 4;
hence z in P by A39; :: thesis:

end;

hence z in the topology of S by A5, A32, TARSKI:2; :: thesis:

end;

for z being object st z in ContinuousFunctions (S,T) holds
z in Funcs ( the carrier of M, the carrier of T)

proof

let z be object ; :: thesis:
assume z in ContinuousFunctions (S,T) ; :: thesis:
then ex f being Function of the carrier of S, the carrier of T st
( z = f & f is continuous ) ;
hence z in Funcs ( the carrier of M, the carrier of T) by FUNCT_2:8, A6, A2; :: thesis:

end;

then ContinuousFunctions (S,T) c= Funcs ( the carrier of M, the carrier of T) ;
then reconsider H = G as Subset of (Funcs ( the carrier of M, the carrier of T)) by XBOOLE_1:1;
S = TopSpaceMetr M by A2, A7, A6, TARSKI:2;
then A40: ( Cl G is compact iff ( H is equibounded & H is equicontinuous ) ) by Th28, A3;
consider K, D being Real such that
A41: ( 0 < K & 0 < D & ( for F being Function of X,T st F in G holds
( ( for x, y being Point of RNS st x in X & y in X holds
||.((F /. x) - (F /. y)).|| <= D * ||.(x - y).|| ) & ( for x being Point of RNS st x in X holds
||.(F /. x).|| <= K ) ) ) ) by A4;
A42: for f being Function of the carrier of M, the carrier of T st f in H holds
for x being Element of M holds ||.(f . x).|| <= K

proof

let f be Function of the carrier of M, the carrier of T; :: thesis:
assume A43: f in H ; :: thesis:
reconsider F = f as Function of X, the carrier of T by A6;
let x be Element of M; :: thesis:
reconsider x1 = x as Point of (MetricSpaceNorm RNS) by TARSKI:def 3, A6;
reconsider x2 = x1 as Point of RNS ;
dom F = X by FUNCT_2:def 1;
then F /. x2 = f . x by A6, PARTFUN1:def 6;
hence ||.(f . x).|| <= K by A41, A43, A6; :: thesis:

end;

for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in H holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) )

proof

let e be Real; :: thesis:
assume A45: 0 < e ; :: thesis:
set d = e / D;
take e / D ; :: thesis:
thus 0 < e / D by A41, A45, XREAL_1:139; :: thesis:
let f be Function of the carrier of M, the carrier of T; :: thesis:
assume A46: f in H ; :: thesis:
reconsider F = f as Function of X, the carrier of T by A6;
let x, y be Element of M; :: thesis:
assume A47: dist (x,y) < e / D ; :: thesis:
reconsider x1 = x, y1 = y as Point of (MetricSpaceNorm RNS) by TARSKI:def 3, A6;
reconsider x2 = x1, y2 = y1 as Point of RNS ;
A48: dom F = X by FUNCT_2:def 1;
then A49: F /. x2 = f . x by A6, PARTFUN1:def 6;
F /. y2 = f . y by A6, A48, PARTFUN1:def 6;
then A50: ||.((f . x) - (f . y)).|| <= D * ||.(x2 - y2).|| by A6, A41, A46, A49;
dist (x1,y1) < e / D by A47, TOPMETR:def 1;
then ||.(x2 - y2).|| < e / D by NORMSP_2:def 1;
then D * ||.(x2 - y2).|| < D * (e / D) by XREAL_1:68, A41;
then D * ||.(x2 - y2).|| < e by A41, XCMPLX_1:87;
hence ||.((f . x) - (f . y)).|| < e by A50, XXREAL_0:2; :: thesis:

end;

hence Cl G is compact by A40, A42; :: thesis: