theorem
for
n being
Nat for
k being
FinSequence of
NAT for
S being non
empty strict compact TopSpace for
X being non
empty Subset of
(REAL-NS (k . 1)) for
T being
NormedLinearTopSpace st
S is
SubSpace of
TopSpaceNorm (REAL-NS (k . 1)) & the
carrier of
S = 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 non
empty Subset of
(R_NormSpace_of_ContinuousFunctions (S,T)) st
G c= { (f | X) where f is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : f in NEURONS (n,k) } & 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
(REAL-NS (k . 1)) st
x in X &
y in X holds
||.((F /. x) - (F /. y)).|| <= D * ||.(x - y).|| ) & ( for
x being
Point of
(REAL-NS (k . 1)) st
x in X holds
||.(F /. x).|| <= K ) ) ) ) holds
Cl G is
compact by Th29;