for G being Group
for a being FinSequence of G st ( for i being object st i in dom a holds
a . i = 1_ G ) holds
Product a = 1_ G