theorem Th1: :: GROUP_3:1

for G being Group
for a, b being Element of G holds
( (a * b) * (b ") = a & (a * (b ")) * b = a & ((b ") * b) * a = a & (b * (b ")) * a = a & a * (b * (b ")) = a & a * ((b ") * b) = a & (b ") * (b * a) = a & b * ((b ") * a) = a )