theorem Th4: :: FINSOP_1:4

for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)