let M be non empty MetrSpace; :: thesis: for S being non empty compact TopSpace
for T being non empty MetrSpace
for U being compact Subset of (TopSpaceMetr T)
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 & ( for f being Function st f in F holds
rng f c= U ) holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )
let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace
for U being compact Subset of (TopSpaceMetr T)
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 & ( for f being Function st f in F holds
rng f c= U ) holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )
let T be non empty MetrSpace; :: thesis: for U being compact Subset of (TopSpaceMetr T)
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 & ( for f being Function st f in F holds
rng f c= U ) holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )
let U be compact Subset of (TopSpaceMetr T); :: 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 & ( for f being Function st f in F holds
rng f c= U ) holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )
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 & ( for f being Function st f in F holds
rng f c= U ) holds
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )
let G be Subset of (Funcs ( the carrier of M, the carrier of T)); :: thesis: ( S = TopSpaceMetr M & T is complete & G = F & ( for f being Function st f in F holds
rng f c= U ) implies ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous ) )
assume that
A1: S = TopSpaceMetr M and
A2: T is complete ; :: thesis: ( not G = F or ex f being Function st
( f in F & not rng f c= U ) or ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous ) )
assume A3: ( G = F & ( for f being Function st f in F holds
rng f c= U ) ) ; :: thesis: ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )
set Z = MetricSpace_of_ContinuousFunctions (S,T);
( Cl F is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | F is totally_bounded ) by Th14, A2;
then ( (MetricSpace_of_ContinuousFunctions (S,T)) | F is totally_bounded iff (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact ) by TOPMETR4:14;
hence ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact implies G is equicontinuous ) by A1, Th15, A3; :: thesis: ( G is equicontinuous implies (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact )
assume A5: G is equicontinuous ; :: thesis: (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact
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

proof

let x be Point of S; :: thesis: 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 Fx be non empty Subset of T; :: thesis: ( Fx = { (f . x) where f is Function of S,T : f in F } implies T | (Cl Fx) is compact )
assume A6: Fx = { (f . x) where f is Function of S,T : f in F } ; :: thesis: T | (Cl Fx) is compact
A7: Fx c= U

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Fx or y in U )
assume y in Fx ; :: thesis: y in U
then consider f being Function of S,T such that
A8: ( y = f . x & f in F ) by A6;
A9: f . x in rng f by FUNCT_2:4;
rng f c= U by A3, A8;
hence y in U by A8, A9; :: thesis: verum

end;

consider Gx being Subset of (TopSpaceMetr T) such that
A10: ( Fx = Gx & Cl Fx = Cl Gx ) by ASCOLI:def 1;
reconsider HClx = Cl Gx as non empty Subset of T by A10;
A11: TopSpaceMetr T is T_2 by PCOMPS_1:34;
Cl Gx c= Cl U by A7, A10, PRE_TOPC:19;
then Cl Gx c= U by A11, PRE_TOPC:22;
then Cl Gx is compact by COMPTS_1:9;
then HClx is sequentially_compact by TOPMETR4:15;
hence T | (Cl Fx) is compact by A10, TOPMETR4:14; :: thesis: verum

end;

hence (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact by Th19, A1, A2, A3, A5; :: thesis: verum