let M be non empty MetrSpace; :: thesis: for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) )
let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) )
let T be NormedLinearTopSpace; :: thesis: ( S = TopSpaceMetr M & T is complete & T is finite-dimensional & dim T <> 0 implies for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) ) )
assume that
A1: S = TopSpaceMetr M and
A2: T is complete and
A3: ( T is finite-dimensional & dim T <> 0 ) ; :: thesis: for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis: for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st G = H holds
( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) )
let H be non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))); :: thesis: ( G = H implies ( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) ) )
assume G = H ; :: thesis: ( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) )
then ( (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded iff ( G is equibounded & G is equicontinuous ) ) by Th26, A1, A2, A3;
hence ( Cl H is sequentially_compact iff ( G is equibounded & G is equicontinuous ) ) by ASCOLI:11, A2; :: thesis: verum