theorem :: NEURONS1:32

for n being Nat
for k being FinSequence of NAT
for S being non empty strict compact TopSpace
for M being non empty SubSpace of MetricSpaceNorm (REAL-NS (k . 1))
for X being non empty Subset of (REAL-NS (k . 1))
for T being NormedLinearTopSpace st S = TopSpaceMetr M & the carrier of M = X & X is compact & T is complete & T is finite-dimensional & dim T <> 0 & REAL-NS (k . (n + 1)) = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) st G = F & G c= { (f | X) where f is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : f in NEURONS (n,k) } holds
( Cl F is compact iff ( G is equibounded & G is equicontinuous ) ) by Th28;