let c, d be Real; ( 0 < c implies rseq (1,0,c,d) is convergent )
assume A1:
0 < c
; rseq (1,0,c,d) is convergent
take
1 / c
; SEQ_2:def 6 for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= |.(((rseq (1,0,c,d)) . b3) - (1 / c)).| ) )
thus
for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= |.(((rseq (1,0,c,d)) . b3) - (1 / c)).| ) )
by A1, Lm9; verum