for K being non empty associative commutative well-unital doubleLoopStr
for p, q being FinSequence of the carrier of K holds p "*" q = q "*" p by Th64;