theorem ringext: :: FIELD_11:4

for R being non degenerated comRing
for S being comRingExtension of R
for n being Ordinal holds Polynom-Ring (n,S) is comRingExtension of Polynom-Ring (n,R)