let R be non degenerated Ring; :: thesis: for S being RingExtension of R
for a being Element of R
for b being Element of S st a = b holds
rpoly (1,a) = rpoly (1,b)
let S be RingExtension of R; :: thesis: for a being Element of R
for b being Element of S st a = b holds
rpoly (1,a) = rpoly (1,b)
let a be Element of R; :: thesis: for b being Element of S st a = b holds
rpoly (1,a) = rpoly (1,b)
let b be Element of S; :: thesis: ( a = b implies rpoly (1,a) = rpoly (1,b) )
assume A1: a = b ; :: thesis: rpoly (1,a) = rpoly (1,b)
A2: R is Subring of S by Def1;
A3: the carrier of (Polynom-Ring R) c= the carrier of (Polynom-Ring S) by Th6;
set q = rpoly (1,b);
reconsider p = rpoly (1,a) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider p = p as Element of the carrier of (Polynom-Ring S) by A3;
reconsider p = p as Polynomial of S ;
len (rpoly (1,b)) > 0 by UPROOTS:17;
then A4: (len (rpoly (1,b))) -' 1 = (len (rpoly (1,b))) - 1 by XREAL_0:def 2;
then reconsider lenq = (len (rpoly (1,b))) - 1 as Element of NAT ;
A5: 1 = deg (rpoly (1,b)) by HURWITZ:27
.= (len (rpoly (1,b))) - 1 by HURWITZ:def 2 ;
then A6: len (rpoly (1,b)) = 1 + 1 ;

A7: now :: thesis: for i being Nat st i >= len (rpoly (1,b)) holds
p . i = 0. S

let i be Nat; :: thesis: ( i >= len (rpoly (1,b)) implies p . i = 0. S )
assume A8: i >= len (rpoly (1,b)) ; :: thesis: p . i = 0. S
reconsider j = i as Element of NAT by ORDINAL1:def 12;
( j <> 0 & j <> 1 ) by A8, A6;
then (rpoly (1,a)) . j = 0. R by HURWITZ:26;
hence p . i = 0. S by A2, C0SP1:def 3; :: thesis: verum

end;

now :: thesis: for m being Nat st m is_at_least_length_of p holds
len (rpoly (1,b)) <= m

let m be Nat; :: thesis: ( m is_at_least_length_of p implies len (rpoly (1,b)) <= m )
assume A9: m is_at_least_length_of p ; :: thesis: len (rpoly (1,b)) <= m
reconsider j = lenq as Element of NAT ;

now :: thesis: not len (rpoly (1,b)) > m

assume len (rpoly (1,b)) > m ; :: thesis: contradiction
then lenq + 1 > m ;
then lenq >= m by NAT_1:13;
then A10: p . ((len (rpoly (1,b))) -' 1) = 0. S by A4, A9, ALGSEQ_1:def 2;
(rpoly (1,a)) . 1 = 1_ R by HURWITZ:25
.= 1. S by A2, C0SP1:def 3 ;
hence contradiction by A10, A5, XREAL_0:def 2; :: thesis: verum

end;

hence len (rpoly (1,b)) <= m ; :: thesis: verum

end;

then A11: len p = len (rpoly (1,b)) by A7, ALGSEQ_1:def 3, ALGSEQ_1:def 2;

now :: thesis: for k being Nat st k < len (rpoly (1,b)) holds
p . k = (rpoly (1,b)) . k

let k be Nat; :: thesis: ( k < len (rpoly (1,b)) implies p . b₁ = (rpoly (1,b)) . b₁ )
assume A12: k < len (rpoly (1,b)) ; :: thesis: p . b₁ = (rpoly (1,b)) . b₁
(len (rpoly (1,b))) - 1 = deg (rpoly (1,b)) by HURWITZ:def 2
.= 1 by HURWITZ:27 ;
then k < 1 + 1 by A12;
then A13: k <= 1 by NAT_1:13;

per cases ( k = 0 or k <> 0 ) ;

suppose A14: k = 0 ; :: thesis: p . b₁ = (rpoly (1,b)) . b₁

then A15: (rpoly (1,a)) . k = - ((power R) . (a,(0 + 1))) by HURWITZ:25
.= - (((power R) . (a,0)) * a) by GROUP_1:def 7
.= - ((1_ R) * a) by GROUP_1:def 7
.= - b by A1, Lm2 ;
(rpoly (1,b)) . k = - ((power S) . (b,(0 + 1))) by A14, HURWITZ:25
.= - (((power S) . (b,0)) * b) by GROUP_1:def 7
.= - ((1_ S) * b) by GROUP_1:def 7
.= - b ;
hence p . k = (rpoly (1,b)) . k by A15; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: p . b₁ = (rpoly (1,b)) . b₁

then k + 1 > 0 + 1 by XREAL_1:6;
then A16: k >= 1 by NAT_1:13;
then A17: k = 1 by A13, XXREAL_0:1;
(rpoly (1,a)) . 1 = 1_ R by HURWITZ:25
.= 1. S by A2, C0SP1:def 3 ;
hence p . k = 1_ S by A16, A13, XXREAL_0:1
.= (rpoly (1,b)) . k by A17, HURWITZ:25 ;
:: thesis: verum

end;

end;

end;

hence rpoly (1,a) = rpoly (1,b) by A11, ALGSEQ_1:12; :: thesis: verum