let R, S be Ring; :: thesis: ( S is RingExtension of R implies 0_. S = 0_. R )
assume A1: S is R -extending Ring ; :: thesis: 0_. S = 0_. R
thus 0_. S = 0. (Polynom-Ring S) by POLYNOM3:def 10
.= 0. (Polynom-Ring R) by A1, Th7
.= 0_. R by POLYNOM3:def 10 ; :: thesis: verum