theorem ThCommutationEq2: :: GROUP_24:91

for G being strict commutative Group
for a, b being Element of (INT.Group 2) st a = 1 & b = 1 holds
((inversions G) . b) * ((inversions G) . a) = (inversions G) . (a * b)