:: deftheorem dsf defines SeqField FIELD_12:def 8 :
for f being Field-yielding ascending sequence
for b₂ being strict doubleLoopStr holds
( b₂ = SeqField f iff ( the carrier of b₂ = Carrier f & the addF of b₂ = addseq f & the multF of b₂ = multseq f & the OneF of b₂ = 1. (f . 0) & the ZeroF of b₂ = 0. (f . 0) ) );