let c, d be Real; :: thesis: ( 0 < c implies rseq (0,1,c,d) is convergent )
set f = rseq (0,1,c,d);
assume A1: 0 < c ; :: thesis: rseq (0,1,c,d) is convergent
take 0 ; :: according to SEQ_2:def 6 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.(((rseq (0,1,c,d)) . b₃) - 0).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((rseq (0,1,c,d)) . b₂) - 0).| ) )
assume 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((rseq (0,1,c,d)) . b₂) - 0).| )
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p by A1, Lm4;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= |.(((rseq (0,1,c,d)) . b₁) - 0).| )
thus for b₁ being set holds
( not n <= b₁ or not p <= |.(((rseq (0,1,c,d)) . b₁) - 0).| ) by A2; :: thesis: verum