theorem Th24: :: MATRIX_7:25

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