let r2 be Real; :: thesis: ( 0< r2 implies ex n being Nat st for m being Nat st n <= m holds |.((seq1 . m)-(r - r1)).|< r2 ) assume 0< r2
; :: thesis: ex n being Nat st for m being Nat st n <= m holds |.((seq1 . m)-(r - r1)).|< r2 then consider n being Nat such that A5:
for m being Nat st n <= m holds |.((seq . m)- r1).|< r2
byA3; take n = n; :: thesis: for m being Nat st n <= m holds |.((seq1 . m)-(r - r1)).|< r2