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

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