for R being Ring
for S being Subring of R
for F being FinSequence of R
for G being FinSequence of S st F = G holds
Product F = Product G