let X be RealNormSpace; :: thesis: for Sq being sequence of X st Sq is CCauchy holds
ex N being V161() sequence of NAT st
for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)
let Sq be sequence of X; :: thesis: ( Sq is CCauchy implies ex N being V161() sequence of NAT st
for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) )
assume AS: Sq is CCauchy ; :: thesis: ex N being V161() sequence of NAT st
for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)
1 = 2 to_power (- 0) by POWER:29;
then consider N0 being Element of NAT such that
P1: for j, i being Element of NAT st j >= N0 & i >= N0 holds
||.((Sq . j) - (Sq . i)).|| < 2 to_power (- 0) by AS, RSSPACE3:10;
defpred S₁[ set , set , set ] means ex n, x, y being Element of NAT st
( n = $1 & x = $2 & y = $3 & ( ( for j being Element of NAT st j >= x holds
||.((Sq . j) - (Sq . x)).|| < 2 to_power (- n) ) implies ( x < y & ( for j being Element of NAT st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) ) ) );
P2: for n, x being Element of NAT ex y being Element of NAT st S₁[n,x,y]

proof

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

now

assume for j being Element of 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 Element of NAT st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) ) )
0 < 2 to_power (- (n + 1)) by POWER:39;
then consider N2 being Element of NAT such that
P22: for j, i being Element of NAT st j >= N2 & i >= N2 holds
||.((Sq . j) - (Sq . i)).|| < 2 to_power (- (n + 1)) by AS, RSSPACE3:10;
set y = (max (x,N2)) + 1;
take y = (max (x,N2)) + 1; :: thesis: ( x < y & ( for j being Element of 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 Element of NAT st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1))
N2 <= max (x,N2) by XXREAL_0:25;
then P24: N2 < y by NAT_1:13;
thus for j being Element of NAT st j >= y holds
||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) :: thesis: verum

proof

let j be Element of 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 P24, XXREAL_0:2;
hence ||.((Sq . j) - (Sq . y)).|| < 2 to_power (- (n + 1)) by P22; :: thesis: verum

end;

end;

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

end;

consider f being Function of NAT,NAT such that
P3: ( f . 0 = N0 & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(P2);
defpred S₂[ Element of NAT ] means for j being Element of NAT st j >= f . $1 holds
||.((Sq . j) - (Sq . (f . $1))).|| < 2 to_power (- $1);
P5: S₂[ 0 ] by P1, P3;

P6: now

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

end;

P4: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(P5, P6);
P7: f is Real_Sequence by FUNCT_2:9;

now

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

end;

then f is V161() by P7, SEQM_3:def 11;
hence ex N being V161() sequence of NAT st
for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) by P4; :: thesis: verum