:: deftheorem Def1 defines FlattenSeq PRE_POLY:def 1 :
for D being set
for F being FinSequence of D *
for b₃ being Element of D * holds
( b₃ = FlattenSeq F iff ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b₃ = g "**" F ) );