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

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