theorem Th29: :: NEURONS1:29

for RNS being RealNormSpace
for T being NormedLinearTopSpace
for X being non empty Subset of RNS
for S being non empty strict compact TopSpace
for G being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st S is SubSpace of TopSpaceNorm RNS & the carrier of S = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & 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 ) ) ) ) holds
Cl G is compact