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