let M be non empty MetrSpace; :: thesis: for S being non empty compact TopSpace
for T being non empty MetrSpace
for F being non empty Subset of (MetricSpace_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
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )
let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace
for F being non empty Subset of (MetricSpace_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
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )
let T be non empty MetrSpace; :: thesis: for F being non empty Subset of (MetricSpace_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
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )
let F be non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)); :: thesis: for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis: ( S = TopSpaceMetr M & T is complete & G = F implies ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) ) )
assume A1: ( S = TopSpaceMetr M & T is complete ) ; :: thesis: ( not G = F or ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) ) )
assume A2: G = F ; :: thesis: ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )
set Z = MetricSpace_of_ContinuousFunctions (S,T);
A3: ( Cl F is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | F is totally_bounded ) by Th14, A1;
( Cl F is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact ) by TOPMETR4:14;
hence ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) ) by A1, A2, Th17, A3; :: thesis: verum