theorem Th9: :: FIELD_4:13

for R, S being Ring st S is RingExtension of R holds
1. (Polynom-Ring S) = 1. (Polynom-Ring R)