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