for G being Group
for H being Subgroup of G
for F being FinSequence of the carrier of G st rng F c= carr H holds
Product F in H