let Z be RealNormSpace; :: thesis: for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete holds
(MetricSpaceNorm Z) | (Cl H) is complete
let H be non empty Subset of (MetricSpaceNorm Z); :: thesis: ( Z is complete implies (MetricSpaceNorm Z) | (Cl H) is complete )
assume A1: Z is complete ; :: thesis: (MetricSpaceNorm Z) | (Cl H) is complete
reconsider F = H as non empty Subset of Z ;
A2: Cl F = Cl H by Th1;
set N = (MetricSpaceNorm Z) | (Cl H);
A3: the carrier of ((MetricSpaceNorm Z) | (Cl H)) = Cl H by TOPMETR:def 2;
for S2 being sequence of ((MetricSpaceNorm Z) | (Cl H)) st S2 is Cauchy holds
S2 is convergent
proof
let S2 be sequence of ((MetricSpaceNorm Z) | (Cl H)); :: thesis: ( S2 is Cauchy implies S2 is convergent )
assume A4: S2 is Cauchy ; :: thesis: S2 is convergent
A5: rng S2 c= Cl H by A3;
rng S2 c= the carrier of (MetricSpaceNorm Z) by A3, XBOOLE_1:1;
then reconsider S1 = S2 as sequence of (MetricSpaceNorm Z) by FUNCT_2:6;
reconsider seq2 = S1 as sequence of Z ;
A6: rng seq2 c= Cl F by Th1, A5;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r
proof
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r
then consider p being Nat such that
A7: for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r by A4;
take p ; :: thesis: for n, m being Nat st n >= p & m >= p holds
||.((seq2 . n) - (seq2 . m)).|| < r
let n, m be Nat; :: thesis: ( n >= p & m >= p implies ||.((seq2 . n) - (seq2 . m)).|| < r )
assume ( p <= n & p <= m ) ; :: thesis: ||.((seq2 . n) - (seq2 . m)).|| < r
then dist ((S2 . n),(S2 . m)) < r by A7;
then dist ((S1 . n),(S1 . m)) < r by TOPMETR:def 1;
hence ||.((seq2 . n) - (seq2 . m)).|| < r by NORMSP_2:def 1; :: thesis: verum
end;
then A8: seq2 is convergent by A1, RSSPACE3:8;
then lim seq2 in Cl F by NFCONT_1:def 3, A6;
then reconsider L = lim seq2 as Point of ((MetricSpaceNorm Z) | (Cl H)) by TOPMETR:def 2, A2;
reconsider L0 = L as Point of (MetricSpaceNorm Z) ;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq2 . n) - (lim seq2)).|| < r by A8, NORMSP_1:def 7;
then A9: S1 is_convergent_in_metrspace_to L0 by NORMSP_2:4;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r
proof
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
dist ((S2 . n),L) < r
then consider m being Nat such that
A10: for n being Nat st m <= n holds
dist ((S1 . n),L0) < r by METRIC_6:def 2, A9;
take m ; :: thesis: for n being Nat st m <= n holds
dist ((S2 . n),L) < r
let n be Nat; :: thesis: ( m <= n implies dist ((S2 . n),L) < r )
assume m <= n ; :: thesis: dist ((S2 . n),L) < r
then dist ((S1 . n),L0) < r by A10;
hence dist ((S2 . n),L) < r by TOPMETR:def 1; :: thesis: verum
end;
hence S2 is convergent ; :: thesis: verum
end;
hence (MetricSpaceNorm Z) | (Cl H) is complete ; :: thesis: verum