let R be Ring; :: thesis: for S being RingExtension of R holds 1_. S = 1_. R
let S be R -extending Ring; :: thesis: 1_. S = 1_. R
thus 1_. S = 1. (Polynom-Ring S) by POLYNOM3:def 10
.= 1. (Polynom-Ring R) by Th9
.= 1_. R by POLYNOM3:def 10 ; :: thesis: verum