theorem Th7: :: FINSOP_1:7

for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G