let M be non empty MetrSpace; for S being non empty compact TopSpace
for T being NormedLinearTopSpace
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 S = TopSpaceMetr M & T is complete & G = H holds
( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) )
let S be non empty compact TopSpace; for T being NormedLinearTopSpace
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 S = TopSpaceMetr M & T is complete & G = H holds
( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) )
let T be NormedLinearTopSpace; 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 S = TopSpaceMetr M & T is complete & G = H holds
( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) )
let G be 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 S = TopSpaceMetr M & T is complete & G = H holds
( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) )
let H be non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))); ( S = TopSpaceMetr M & T is complete & G = H implies ( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) ) )
assume A1:
( S = TopSpaceMetr M & T is complete )
; ( not G = H or ( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) ) )
assume A2:
G = H
; ( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) )
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
( (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded iff Cl H is sequentially_compact )
by A1, Th11;
hence
( Cl H is sequentially_compact iff ( G is equicontinuous & ( for x being Point of S
for Hx being non empty Subset of (MetricSpaceNorm T) st Hx = { (f . x) where f is Function of S,T : f in H } holds
(MetricSpaceNorm T) | (Cl Hx) is compact ) ) )
by A1, A2, Th16; verum