let X be RealNormSpace; :: thesis: for Sq being sequence of X st Sq is Cauchy_sequence_by_Norm holds

ex N being V174() 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 V174() 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 V174() 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_{1}[ 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_{1}[n,x,y]

A6: ( f . 0 = N0 & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A3);

defpred S_{2}[ Nat] means for j being Nat st j >= f . $1 holds

||.((Sq . j) - (Sq . (f . $1))).|| < 2 to_power (- $1);

A7: S_{2}[ 0 ]
by A2, A6;

_{2}[i]
from NAT_1:sch 2(A7, A8);

hence ex N being V174() 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

ex N being V174() 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 V174() 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 V174() 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

( 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

proof

consider f being sequence of NAT such that
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S_{1}[n,x,y]

let x be Element of NAT ; :: thesis: ex y being Element of NAT st S_{1}[n,x,y]

_{1}[n,x,y]
; :: thesis: verum

end;let x be Element of NAT ; :: thesis: ex y being Element of NAT st S

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)) ) ) )

hence
ex y being Element of NAT st S||.((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

end;||.((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;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

A6: ( f . 0 = N0 & ( for n being Nat holds S

defpred S

||.((Sq . j) - (Sq . (f . $1))).|| < 2 to_power (- $1);

A7: S

A8: now :: thesis: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]

A10:
for i being Nat holds SS

let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A9: S_{2}[i]
; :: thesis: S_{2}[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_{2}[i + 1]
by A9; :: thesis: verum

end;assume A9: S

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

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

then
f is V174()
;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;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

hence ex N being V174() 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