assume A10:
for n being Nat holds the Element of Omega in ASeq . n
; :: thesis: for n being Nat holds (P * ASeq). n = 1
for n being Nat holds (P * ASeq). n = 1
assume
not for n being Nat holds the Element of Omega in ASeq . n
; :: thesis: ex m being Nat st for n being Nat st m <= n holds (P * ASeq). n =0 then consider m being Nat such that A14:
not the Element of Omega in ASeq . m
; take
m
; :: thesis: for n being Nat st m <= n holds (P * ASeq). n =0
for n being Nat st m <= n holds (P * ASeq). n =0
assume A19:
for n being Nat holds (P * ASeq). n = 1
; :: thesis: ( P * ASeq is convergent & lim(P * ASeq)= 1 )
ex m being Nat st for n being Nat st m <= n holds (P * ASeq). n = r