let R, S be Ring; :: thesis: ( S is RingExtension of R implies 1. (Polynom-Ring S) = 1. (Polynom-Ring R) )
assume A1: S is R -extending Ring ; :: thesis: 1. (Polynom-Ring S) = 1. (Polynom-Ring R)
then A2: R is Subring of S by Def1;
thus 1. (Polynom-Ring R) = 1_. R by POLYNOM3:def 10
.= (0_. R) +* (0,(1. R)) by POLYNOM3:def 8
.= (0_. R) +* (0,(1. S)) by A2, C0SP1:def 3
.= (0_. S) +* (0,(1. S)) by A1, Th8
.= 1_. S by POLYNOM3:def 8
.= 1. (Polynom-Ring S) by POLYNOM3:def 10 ; :: thesis: verum