let vseq be sequence of linfty_Space; :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent
defpred S1[ object , object ] means ex i being Nat st
( $1 = i & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in REAL & S1[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in REAL & S1[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )
then reconsider i = x as Nat ;
deffunc H1( Nat) -> set = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A3: for n being Nat holds rseqi . n = H1(n) from SEQ_1:sch 1();
 reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr ; :: thesis: ( lr in REAL & S1[x,lr] )
now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e )
assume A4: e > 0 ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
thus ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e :: thesis: verum
proof
consider k being Nat such that
A5: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, RSSPACE3:8;
take k ; :: thesis: for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
let m be Nat; :: thesis: ( k <= m implies |.((rseqi . m) - (rseqi . k)).| < e )
assume A6: k <= m ; :: thesis: |.((rseqi . m) - (rseqi . k)).| < e
seq_id ((vseq . m) - (vseq . k)) is bounded by Def1;
then A7: |.(seq_id ((vseq . m) - (vseq . k))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Lm2;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:7
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:10
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then A8: |.((rseqi . m) - (rseqi . k)).| = (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:12;
||.((vseq . m) - (vseq . k)).|| = upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Th2;
then upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) < e by A5, A6;
hence |.((rseqi . m) - (rseqi . k)).| < e by A7, A8, XXREAL_0:2; :: thesis: verum
end;
end;
then rseqi is convergent by SEQ_4:41;
hence ( lr in REAL & S1[x,lr] ) by A3; :: thesis: verum
end;
consider f being sequence of REAL such that
A9: for x being object st x in NAT holds
S1[x,f . x] from FUNCT_2:sch 1(A2);
 reconsider tseq = f as Real_Sequence ;
A10: now :: thesis: for i being Nat ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
let i be Nat; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
i in NAT by ORDINAL1:def 12;
then ex i0 being Nat st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A9;
hence ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: thesis: verum
end;
A11: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
proof
let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A12: e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
reconsider e = e as Real ;
consider k being Nat such that
A13: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A12, RSSPACE3:8;
A14: for m, n being Nat st n >= k & m >= k holds
( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e )
proof
let m, n be Nat; :: thesis: ( n >= k & m >= k implies ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) )
assume ( n >= k & m >= k ) ; :: thesis: ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e )
then A15: ||.((vseq . n) - (vseq . m)).|| < e by A13;
seq_id ((vseq . n) - (vseq . m)) is bounded by Def1;
hence ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & upper_bound (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) by A15, Def2; :: thesis: verum
end;
A16: for n, i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
proof
let n be Nat; :: thesis: for i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
A17: for m, k being Nat holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
proof
let m, k be Nat; :: thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) ; :: thesis: verum
end;
now :: thesis: for i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
let i be Nat; :: thesis: for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
consider rseqi being Real_Sequence such that
A18: for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i and
A19: ( rseqi is convergent & tseq . i = lim rseqi ) by A10;
now :: thesis: for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
let rseq be Real_Sequence; :: thesis: ( ( for m being Nat holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) implies ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) )
assume A20: for m being Nat holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ; :: thesis: ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
A21: now :: thesis: for m being Nat holds rseq . m = |.((rseqi . m) - ((seq_id (vseq . n)) . i)).|
let m be Nat; :: thesis: rseq . m = |.((rseqi . m) - ((seq_id (vseq . n)) . i)).|
A22: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A17;
thus rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A20
.= |.((seq_id ((vseq . m) - (vseq . n))) . i).| by SEQ_1:12
.= |.(((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)).| by A22, RFUNCT_2:1
.= |.((rseqi . m) - ((seq_id (vseq . n)) . i)).| by A18 ; :: thesis: verum
end;
|.((tseq . i) - ((seq_id (vseq . n)) . i)).| = |.((tseq - (seq_id (vseq . n))) . i).| by RFUNCT_2:1
.= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i by SEQ_1:12 ;
hence ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A19, A21, RSSPACE3:1; :: thesis: verum
end;
hence for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; :: thesis: verum
end;
hence for i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; :: thesis: verum
end;
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
proof
let n be Nat; :: thesis: ( n >= k implies ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A23: n >= k ; :: thesis: ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
A24: for i being Nat holds (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e
proof
let i be Nat; :: thesis: (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e
deffunc H1( Nat) -> set = (abs (seq_id ((vseq . $1) - (vseq . n)))) . i;
consider rseq being Real_Sequence such that
A25: for m being Nat holds rseq . m = H1(m) from SEQ_1:sch 1();
 A26: for m being Nat st m >= k holds
rseq . m <= e
proof
let m be Nat; :: thesis: ( m >= k implies rseq . m <= e )
A27: rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A25;
assume A28: m >= k ; :: thesis: rseq . m <= e
then abs (seq_id ((vseq . m) - (vseq . n))) is bounded by A14, A23;
then A29: (abs (seq_id ((vseq . m) - (vseq . n)))) . i <= upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . n))))) by Lm2;
upper_bound (rng (abs (seq_id ((vseq . m) - (vseq . n))))) <= e by A14, A23, A28;
hence rseq . m <= e by A29, A27, XXREAL_0:2; :: thesis: verum
end;
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A16, A25;
hence (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e by A26, RSSPACE2:5; :: thesis: verum
end;
A30: 0 + e < 1 + e by XREAL_1:8;
now :: thesis: for i being Nat holds |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1
let i be Nat; :: thesis: |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1
( (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e & (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i = |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| ) by A24, SEQ_1:12;
hence |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1 by A30, XXREAL_0:2; :: thesis: verum
end;
then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A12, SEQ_2:3;
hence ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) by A24, Lm1; :: thesis: verum
end;
hence ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) ; :: thesis: verum
end;
A31: seq_id tseq is bounded
proof
consider m being Nat such that
A32: for n being Nat st n >= m holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= 1 ) by A11;
A33: abs ((seq_id tseq) - (seq_id (vseq . m))) is bounded by A32;
set d = abs (seq_id tseq);
set b = abs (seq_id (vseq . m));
set a = abs ((seq_id tseq) - (seq_id (vseq . m)));
A34: seq_id (vseq . m) is bounded by Def1;
A35: for i being Nat holds (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
proof
let i be Nat; :: thesis: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
A36: ( (abs (seq_id (vseq . m))) . i = |.((seq_id (vseq . m)) . i).| & (abs (seq_id tseq)) . i = |.((seq_id tseq) . i).| ) by SEQ_1:12;
(abs ((seq_id tseq) - (seq_id (vseq . m)))) . i = |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by SEQ_1:12
.= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by SEQ_1:7
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by SEQ_1:10
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
then ((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i) <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i by A36, COMPLEX1:59;
then (((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i)) + ((abs (seq_id (vseq . m))) . i) <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . i) + ((abs (seq_id (vseq . m))) . i) by XREAL_1:6;
hence (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by SEQ_1:7; :: thesis: verum
end;
abs (seq_id tseq) is bounded
proof
reconsider r = (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 1 as Real ;
(abs (seq_id (vseq . m))) . 1 = |.((seq_id (vseq . m)) . 1).| by SEQ_1:12;
then A37: 0 <= (abs (seq_id (vseq . m))) . 1 by COMPLEX1:46;
A38: (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 0 < (upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))))) + 1 by XREAL_1:8;
A39: now :: thesis: for i being Nat holds |.((seq_id tseq) . i).| < r
let i be Nat; :: thesis: |.((seq_id tseq) . i).| < r
( (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i & ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) ) by A33, A34, A35, Lm2;
then A40: (abs (seq_id tseq)) . i <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by XXREAL_0:2;
(abs (seq_id tseq)) . i = |.((seq_id tseq) . i).| by SEQ_1:12;
hence |.((seq_id tseq) . i).| < r by A38, A40, XXREAL_0:2; :: thesis: verum
end;
(abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 = |.(((seq_id tseq) - (seq_id (vseq . m))) . 1).| by SEQ_1:12;
then ( ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . 1 = ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1) + ((abs (seq_id (vseq . m))) . 1) & 0 <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 ) by COMPLEX1:46, SEQ_1:7;
then 0 <= upper_bound (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by A33, A34, A37, Lm2;
then seq_id tseq is bounded by A39, SEQ_2:3;
hence abs (seq_id tseq) is bounded ; :: thesis: verum
end;
hence seq_id tseq is bounded by SEQM_3:37; :: thesis: verum
end;
A41: tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider tv = tseq as Point of linfty_Space by A31, Def1;
take tv ; :: according to NORMSP_1:def 6 :: thesis: for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= ||.((vseq . b3) - tv).|| ) )
let e1 be Real; :: thesis: ( e1 <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) )
assume A42: e1 > 0 ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| )
set e = e1 / 2;
consider m being Nat such that
A43: for n being Nat st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 ) by A11, A42, XREAL_1:215;
A44: e1 / 2 < e1 by A42, XREAL_1:216;
now :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e1
reconsider u = tseq as VECTOR of linfty_Space by A31, A41, Def1;
let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 )
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e1
then A45: upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 by A43;
reconsider v = vseq . n as VECTOR of linfty_Space ;
seq_id (u - v) = u - v by Th2;
then upper_bound (rng (abs (seq_id (u - v)))) = upper_bound (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) by Th2;
then A46: the normF of linfty_Space . (u - v) <= e1 / 2 by A45, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by NORMSP_1:2 ;
hence ||.((vseq . n) - tv).|| < e1 by A44, A46, XXREAL_0:2; :: thesis: verum
end;
hence ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not e1 <= ||.((vseq . b2) - tv).|| ) ; :: thesis: verum