let X be RealNormSpace; :: thesis: for Sq being sequence of X st Sq is Cauchy_sequence_by_Norm holds
ex N being increasing sequence of NAT st
for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)
let Sq be sequence of X; :: thesis: ( Sq is Cauchy_sequence_by_Norm implies ex N being increasing sequence of NAT st
for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) )
assume A1: Sq is Cauchy_sequence_by_Norm ; :: thesis: ex N being increasing sequence of NAT st
for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)
1 = 2 to_power (- 0) by POWER:24;
then consider N0 being Nat such that
A2: for j, i being Nat st j >= N0 & i >= N0 holds
||.((Sq . j) - (Sq . i)).|| < 2 to_power (- 0) by A1, RSSPACE3:8;
reconsider N0 = N0 as Element of NAT by ORDINAL1:def 12;
defpred S₁[ set , set , set ] means ex n, x, y being Nat st
( n = $1 & x = $2 & y = $3 & ( ( for j being Nat st j >= x holds
||.((Sq . j) - (Sq . x)).|| < 2 to_power (- n) ) implies ( x < y & ( for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) ) ) );
A3: for n being Nat
for x being Element of NAT ex y being Element of NAT st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S₁[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S₁[n,x,y]

now :: thesis: ( ( for j being Nat st j >= x holds
||.((Sq . j) - (Sq . x)).|| < 2 to_power (- n) ) implies ex y being Element of NAT st
( x < y & ( for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) ) )

assume for j being Nat st j >= x holds
||.((Sq . j) - (Sq . x)).|| < 2 to_power (- n) ; :: thesis: ex y being Element of NAT st
( x < y & ( for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) )
0 < 2 to_power (- (n + 1)) by POWER:34;
then consider N2 being Nat such that
A4: for j, i being Nat st j >= N2 & i >= N2 holds
||.((Sq . j) - (Sq . i)).|| < 2 to_power (- (n + 1)) by A1, RSSPACE3:8;
set y = (max (x,N2)) + 1;
take y = (max (x,N2)) + 1; :: thesis: ( x < y & ( for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) )
x <= max (x,N2) by XXREAL_0:25;
hence x < y by NAT_1:13; :: thesis: for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1))
N2 <= max (x,N2) by XXREAL_0:25;
then A5: N2 < y by NAT_1:13;
thus for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) :: thesis: verum

proof

let j be Nat; :: thesis: ( j >= y implies ||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) )
assume j >= y ; :: thesis: ||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1))
then ( j >= N2 & y >= N2 ) by A5, XXREAL_0:2;
hence ||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) by A4; :: thesis: verum

end;

end;

hence ex y being Element of NAT st S₁[n,x,y] ; :: thesis: verum

end;

consider f being sequence of NAT such that
A6: ( f . 0 = N0 & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A3);
defpred S₂[ Nat] means for j being Nat st j >= f . $1 holds
||.((Sq . j) - (Sq . (f . $1))).|| < 2 to_power (- $1);
A7: S₂[ 0 ] by A2, A6;

A8: now :: thesis: for i being Nat st S₂[i] holds
S₂[i + 1]

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A9: S₂[i] ; :: thesis: S₂[i + 1]
ex n, x, y being Nat st
( n = i & x = f . i & y = f . (i + 1) & ( ( for j being Nat st j >= x holds
||.((Sq . j) - (Sq . x)).|| < 2 to_power (- n) ) implies ( x < y & ( for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) ) ) ) by A6;
hence S₂[i + 1] by A9; :: thesis: verum

end;

A10: for i being Nat holds S₂[i] from NAT_1:sch 2(A7, A8);

now :: thesis: for i being Nat holds f . i < f . (i + 1)

let i be Nat; :: thesis: f . i < f . (i + 1)
ex n, x, y being Nat st
( n = i & x = f . i & y = f . (i + 1) & ( ( for j being Nat st j >= x holds
||.((Sq . j) - (Sq . x)).|| < 2 to_power (- n) ) implies ( x < y & ( for j being Nat st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) ) ) ) by A6;
hence f . i < f . (i + 1) by A10; :: thesis: verum

end;

then f is increasing ;
hence ex N being increasing sequence of NAT st
for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) by A10; :: thesis: verum