:: deftheorem defseqp defines seq_p ASYMPT_2:def 2 :
for c being XFinSequence of REAL
for b₂ being Real_Sequence holds
( b₂ = seq_p c iff for x being Nat holds b₂ . x = Sum (c (#) (seq_a^ (x,1,0))) );