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)) for
D,
K being
Real st
0 < D &
0 < K &
G c= { (F | X) where F is Function of (REAL-NS (k . 1)),(REAL-NS (k . (n + 1))) : ex N being non empty FinSequence st
( N is_LayerFunc_Seq D,K,k,n & F = OutPutFunc (N,k,n) ) } holds
Cl G is
compact