:: deftheorem Def8 defines "**" AFINSQ_2:def 8 :
for D being non empty set
for F being XFinSequence st F is D -valued holds
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
for b₄ being Element of D holds
( ( b is having_a_unity & len F = 0 implies ( b₄ = b "**" F iff b₄ = the_unity_wrt b ) ) & ( ( not b is having_a_unity or not len F = 0 ) implies ( b₄ = b "**" F iff ex f being sequence of D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₄ = f . ((len F) - 1) ) ) ) );