for G being Group
for F being FinSequence of the carrier of G holds Product (F - {(1_ G)}) = Product F