theorem Th23: :: MATRIX_7:24

for G being Group
for f being FinSequence of G holds Product (f ^ ((Rev f) ")) = 1_ G