theorem Th7: :: FIELD_4:11

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