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

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