theorem :: FVSUM_1:80

for K being non empty associative commutative well-unital doubleLoopStr
for R being Element of 0 -tuples_on the carrier of K holds Product R = 1. K