theorem Th40: :: AFINSQ_2:40

for D being non empty set
for F being XFinSequence of D
for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)