theorem :: FVSUM_1:79

for K being non empty associative commutative well-unital doubleLoopStr
for a1, a2, a3 being Element of K holds Product <*a1,a2,a3*> = (a1 * a2) * a3