let R, S be Ring; :: thesis: ( S is RingExtension of R implies 0. (Polynom-Ring S) = 0. (Polynom-Ring R) )
assume S is R -extending Ring ; :: thesis: 0. (Polynom-Ring S) = 0. (Polynom-Ring R)
then A1: R is Subring of S by Def1;
thus 0. (Polynom-Ring R) = 0_. R by POLYNOM3:def 10
.= NAT --> (0. R) by POLYNOM3:def 7
.= NAT --> (0. S) by A1, C0SP1:def 3
.= 0_. S by POLYNOM3:def 7
.= 0. (Polynom-Ring S) by POLYNOM3:def 10 ; :: thesis: verum