:: deftheorem defmult defines multseq FIELD_12:def 7 :
for f being Field-yielding ascending sequence
for b₂ being BinOp of (Carrier f) holds
( b₂ = multseq f iff for a, b being Element of Carrier f ex i being Element of NAT ex x, y being Element of (f . i) st
( x = a & y = b & b₂ . (a,b) = x * y ) );