for G being Group
for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Nat st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) "