theorem ThCommutationEq: :: GROUP_24:90

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