let M be non empty MetrSpace; for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F holds
( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
let S be non empty compact TopSpace; for T being NormedLinearTopSpace
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F holds
( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
let T be NormedLinearTopSpace; for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F holds
( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
let F be non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)); for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F holds
( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); ( S = TopSpaceMetr M & T is complete & G = F implies ( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) ) )
assume A1:
( S = TopSpaceMetr M & T is complete )
; ( not G = F or ( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) ) )
assume
G = F
; ( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
then
( Cl F is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
by Th18, A1;
hence
( Cl F is compact iff ( ( for x being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being non empty Subset of (MetricSpaceNorm T) st Fx = { (f . x) where f is Function of S,T : f in F } holds
(MetricSpaceNorm T) | (Cl Fx) is compact ) ) )
by Th5, A1; verum