let c, d be Real; :: thesis: ( 0 < c implies rseq (1,0,c,d) is convergent )
assume A1: 0 < c ; :: thesis: rseq (1,0,c,d) is convergent
take 1 / c ; :: 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 (1,0,c,d)) . b₃) - (1 / c)).| ) )
thus 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 (1,0,c,d)) . b₃) - (1 / c)).| ) ) by A1, Lm9; :: thesis: verum