let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace st T is complete holds
MetricSpace_of_ContinuousFunctions (S,T) is complete
let T be non empty MetrSpace; :: thesis: ( T is complete implies MetricSpace_of_ContinuousFunctions (S,T) is complete )
assume A1: T is complete ; :: thesis: MetricSpace_of_ContinuousFunctions (S,T) is complete
set MSC = MetricSpace_of_ContinuousFunctions (S,T);
set A = ContinuousFunctions (S,T);

now :: thesis: for v being sequence of (MetricSpace_of_ContinuousFunctions (S,T)) st v is Cauchy holds
v is convergent

let v be sequence of (MetricSpace_of_ContinuousFunctions (S,T)); :: thesis: ( v is Cauchy implies v is convergent )
assume a2: v is Cauchy ; :: thesis: v is convergent
then A2: for r being Real st r > 0 holds
ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((v . n),(v . m)) < r ;
defpred S₁[ set , set ] means ex xseq being sequence of T st
for n being Nat holds
( xseq . n = In (((v . n) . $1),T) & xseq is convergent & $2 = lim xseq );
A3: for x being Element of S ex y being Element of T st S₁[x,y]

proof

let x be Element of S; :: thesis: ex y being Element of T st S₁[x,y]
deffunc H₁( Nat) -> Element of the carrier of T = In (((v . $1) . x),T);
consider xseq being sequence of T such that
A4: for n being Element of NAT holds xseq . n = H₁(n) from FUNCT_2:sch 4();
A5: for n being Nat holds xseq . n = H₁(n)

proof

let n be Nat; :: thesis: xseq . n = H₁(n)
n in NAT by ORDINAL1:def 12;
hence xseq . n = H₁(n) by A4; :: thesis: verum

end;

take lx = lim xseq; :: thesis: S₁[x,lx]
A6: for m, k being Nat holds dist ((xseq . m),(xseq . k)) <= dist ((v . m),(v . k))

proof

let m, k be Nat; :: thesis: dist ((xseq . m),(xseq . k)) <= dist ((v . m),(v . k))
( xseq . m = In (((v . m) . x),T) & xseq . k = In (((v . k) . x),T) ) by A5;
hence dist ((xseq . m),(xseq . k)) <= dist ((v . m),(v . k)) by Th11; :: thesis: verum

end;

now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((xseq . n),(xseq . m)) < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((xseq . n),(xseq . m)) < e )
assume A7: e > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((xseq . n),(xseq . m)) < e
consider k being Nat such that
A8: for n, m being Nat st n >= k & m >= k holds
dist ((v . n),(v . m)) < e by A7, a2;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist ((xseq . n),(xseq . m)) < e
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist ((xseq . n),(xseq . m)) < e )
assume ( n >= k & m >= k ) ; :: thesis: dist ((xseq . n),(xseq . m)) < e
then A9: dist ((v . n),(v . m)) < e by A8;
dist ((xseq . n),(xseq . m)) <= dist ((v . n),(v . m)) by A6;
hence dist ((xseq . n),(xseq . m)) < e by A9, XXREAL_0:2; :: thesis: verum

end;

then xseq is Cauchy ;
hence S₁[x,lx] by A1, A5; :: thesis: verum

end;

consider tseq0 being Function of S,T such that
A10: for x being Element of S holds S₁[x,tseq0 . x] from FUNCT_2:sch 3(A3);
reconsider tseq = tseq0 as Function of S,(TopSpaceMetr T) ;
for x being Point of S holds tseq is_continuous_at x

proof

let x be Point of S; :: thesis: tseq is_continuous_at x
consider xseq being sequence of T such that
A11: for n being Nat holds
( xseq . n = In (((v . n) . x),T) & xseq is convergent & tseq0 . x = lim xseq ) by A10;

now :: thesis: for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e ) )

let e be Real; :: thesis: ( 0 < e implies ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e ) ) )
assume A12: 0 < e ; :: thesis: ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e ) )
consider N1 being Nat such that
A13: for n, m being Nat st N1 <= n & N1 <= m holds
dist ((v . n),(v . m)) < e / 4 by a2, A12;
A14: for n, m being Nat st N1 <= n & N1 <= m holds
for x being Point of S holds dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4

proof

let n, m be Nat; :: thesis: ( N1 <= n & N1 <= m implies for x being Point of S holds dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4 )
assume A15: ( N1 <= n & N1 <= m ) ; :: thesis: for x being Point of S holds dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4
let x be Point of S; :: thesis: dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4
A16: dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) <= dist ((v . n),(v . m)) by Th11;
dist ((v . n),(v . m)) < e / 4 by A13, A15;
hence dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4 by A16, XXREAL_0:2; :: thesis: verum

end;

consider N2 being Nat such that
A17: for m being Nat st m >= N2 holds
dist ((xseq . m),(tseq0 . x)) < e / 4 by A11, A12, TBSP_1:def 3;
reconsider N3 = max (N1,N2) as Nat by XXREAL_0:16;
A18: ( N2 <= N3 & N1 <= N3 ) by XXREAL_0:25;
then A19: dist ((xseq . N3),(tseq0 . x)) < e / 4 by A17;
A20: xseq . N3 = In (((v . N3) . x),T) by A11;
v . N3 in ContinuousFunctions (S,T) ;
then consider vN3 being Function of S,(TopSpaceMetr T) such that
A21: ( v . N3 = vN3 & vN3 is continuous ) ;
consider H being Subset of S such that
A22: ( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((vN3 . x),T)),(In ((vN3 . y),T))) < e / 4 ) ) by Th2, A12, TMAP_1:50, A21;
take H = H; :: thesis: ( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e ) )
thus ( H is open & x in H ) by A22; :: thesis: for y being Point of S st y in H holds
dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e
let y be Point of S; :: thesis: ( y in H implies dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e )
assume y in H ; :: thesis: dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e
then A23: dist ((In ((vN3 . x),T)),(In ((vN3 . y),T))) < e / 4 by A22;
consider yseq being sequence of T such that
A24: for n being Nat holds
( yseq . n = In (((v . n) . y),T) & yseq is convergent & tseq0 . y = lim yseq ) by A10;
consider N4 being Nat such that
A25: for m being Nat st m >= N4 holds
dist ((yseq . m),(tseq0 . y)) < e / 4 by A24, A12, TBSP_1:def 3;
reconsider N5 = max (N3,N4) as Nat by XXREAL_0:16;
a26: ( N4 <= N5 & N3 <= N5 ) by XXREAL_0:25;
then A26: N1 <= N5 by A18, XXREAL_0:2;
A27: dist ((yseq . N5),(tseq0 . y)) < e / 4 by a26, A25;
A28: dist ((tseq0 . x),(tseq0 . y)) <= (dist ((tseq0 . x),(yseq . N5))) + (dist ((yseq . N5),(tseq0 . y))) by METRIC_1:4;
A29: dist ((tseq0 . x),(yseq . N5)) <= (dist ((tseq0 . x),(xseq . N3))) + (dist ((xseq . N3),(yseq . N5))) by METRIC_1:4;
A30: dist ((xseq . N3),(yseq . N5)) <= (dist ((xseq . N3),(yseq . N3))) + (dist ((yseq . N3),(yseq . N5))) by METRIC_1:4;
A31: dist ((In (((v . N3) . y),T)),(In (((v . N5) . y),T))) < e / 4 by A14, A18, A26;
yseq . N3 = In (((v . N3) . y),T) by A24;
then A33: dist ((yseq . N3),(yseq . N5)) < e / 4 by A24, A31;
A34: xseq . N3 = In (((v . N3) . x),T) by A20
.= In ((vN3 . x),T) by A21 ;
yseq . N3 = In (((v . N3) . y),T) by A24
.= In ((vN3 . y),T) by A21 ;
then (dist ((xseq . N3),(yseq . N3))) + (dist ((yseq . N3),(yseq . N5))) < (e / 4) + (e / 4) by A23, A34, A33, XREAL_1:8;
then dist ((xseq . N3),(yseq . N5)) < e / 2 by A30, XXREAL_0:2;
then (dist ((tseq0 . x),(xseq . N3))) + (dist ((xseq . N3),(yseq . N5))) < (e / 4) + (e / 2) by A19, XREAL_1:8;
then dist ((tseq0 . x),(yseq . N5)) < (e / 4) + (e / 2) by A29, XXREAL_0:2;
then (dist ((tseq0 . x),(yseq . N5))) + (dist ((yseq . N5),(tseq0 . y))) < ((e / 4) + (e / 2)) + (e / 4) by A27, XREAL_1:8;
hence dist ((In ((tseq . x),T)),(In ((tseq . y),T))) < e by A28, XXREAL_0:2; :: thesis: verum

end;

hence tseq is_continuous_at x by Th2; :: thesis: verum

end;

then tseq is continuous Function of S,(TopSpaceMetr T) by TMAP_1:50;
then tseq in MetricSpace_of_ContinuousFunctions (S,T) ;
then reconsider w = tseq as Point of (MetricSpace_of_ContinuousFunctions (S,T)) ;
for e being Real st e > 0 holds
ex N being Nat st
for m being Nat st N <= m holds
dist ((v . m),w) < e

proof

let e be Real; :: thesis: ( e > 0 implies ex N being Nat st
for m being Nat st N <= m holds
dist ((v . m),w) < e )
assume A36: e > 0 ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
dist ((v . m),w) < e
then consider N1 being Nat such that
A37: for n, m being Nat st N1 <= n & N1 <= m holds
dist ((v . n),(v . m)) < e / 4 by A2;
A38: for n, m being Nat st N1 <= n & N1 <= m holds
for x being Point of S holds dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4

proof

let n, m be Nat; :: thesis: ( N1 <= n & N1 <= m implies for x being Point of S holds dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4 )
assume A39: ( N1 <= n & N1 <= m ) ; :: thesis: for x being Point of S holds dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4
let x be Point of S; :: thesis: dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4
A40: dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) <= dist ((v . n),(v . m)) by Th11;
dist ((v . n),(v . m)) < e / 4 by A37, A39;
hence dist ((In (((v . n) . x),T)),(In (((v . m) . x),T))) < e / 4 by A40, XXREAL_0:2; :: thesis: verum

end;

take N1 ; :: thesis: for m being Nat st N1 <= m holds
dist ((v . m),w) < e
let m be Nat; :: thesis: ( N1 <= m implies dist ((v . m),w) < e )
assume A41: N1 <= m ; :: thesis: dist ((v . m),w) < e
v . m in ContinuousFunctions (S,T) ;
then consider vm being Function of S,(TopSpaceMetr T) such that
A42: ( v . m = vm & vm is continuous ) ;
reconsider vm = vm as Function of S,T ;
for x being Point of S holds dist ((vm . x),(tseq0 . x)) <= e / 2

proof

let x be Point of S; :: thesis: dist ((vm . x),(tseq0 . x)) <= e / 2
consider xseq being sequence of T such that
A43: for n being Nat holds
( xseq . n = In (((v . n) . x),T) & xseq is convergent & tseq0 . x = lim xseq ) by A10;
consider N2 being Nat such that
A44: for m being Nat st m >= N2 holds
dist ((xseq . m),(tseq0 . x)) < e / 4 by A43, A36, TBSP_1:def 3;
reconsider N3 = max (N1,N2) as Nat by XXREAL_0:16;
A45: ( N2 <= N3 & N1 <= N3 ) by XXREAL_0:25;
then A46: dist ((xseq . N3),(tseq0 . x)) < e / 4 by A44;
A47: dist ((In (((v . N3) . x),T)),(In (((v . m) . x),T))) < e / 4 by A41, A45, A38;
A48: xseq . N3 = In (((v . N3) . x),T) by A43;
A49: dist ((In (((v . m) . x),T)),(tseq0 . x)) <= (dist ((In (((v . m) . x),T)),(In (((v . N3) . x),T)))) + (dist ((In (((v . N3) . x),T)),(tseq0 . x))) by METRIC_1:4;
dist ((In (((v . m) . x),T)),(In (((v . N3) . x),T))) < e / 4 by A47;
then (dist ((In (((v . m) . x),T)),(In (((v . N3) . x),T)))) + (dist ((In (((v . N3) . x),T)),(tseq0 . x))) < (e / 4) + (e / 4) by A46, A48, XREAL_1:8;
hence dist ((vm . x),(tseq0 . x)) <= e / 2 by A42, A49, XXREAL_0:2; :: thesis: verum

end;

then A51: dist ((v . m),w) <= e / 2 by Th12, A42;
e / 2 < e by A36, XREAL_1:216;
hence dist ((v . m),w) < e by A51, XXREAL_0:2; :: thesis: verum

end;

hence v is convergent ; :: thesis: verum

end;

hence MetricSpace_of_ContinuousFunctions (S,T) is complete ; :: thesis: verum