:: deftheorem Def10 defines FlattenSeq AFINSQ_2:def 10 :
for D being set
for F being XFinSequence of D ^omega
for b₃ being Element of D ^omega holds
( b₃ = FlattenSeq F iff ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b₃ = g "**" F ) );