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 () c= the carrier of () by Th6;
set q = rpoly (1,b);
reconsider p = rpoly (1,a) as Element of the carrier of () by POLYNOM3:def 10;
reconsider p = p as Element of the carrier of () 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 ; :: 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 ;
(rpoly (1,a)) . 1 = 1_ R by HURWITZ:25
.= 1. S by ;
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 ;
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 . b1 = (rpoly (1,b)) . b1 )
assume A12: k < len (rpoly (1,b)) ; :: thesis: p . b1 = (rpoly (1,b)) . b1
(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 . b1 = (rpoly (1,b)) . b1
then A15: (rpoly (1,a)) . k = - (() . (a,(0 + 1))) by HURWITZ:25
.= - ((() . (a,0)) * a) by GROUP_1:def 7
.= - ((1_ R) * a) by GROUP_1:def 7
.= - b by ;
(rpoly (1,b)) . k = - (() . (b,(0 + 1))) by
.= - ((() . (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 . b1 = (rpoly (1,b)) . b1
then k + 1 > 0 + 1 by XREAL_1:6;
then A16: k >= 1 by NAT_1:13;
then A17: k = 1 by ;
(rpoly (1,a)) . 1 = 1_ R by HURWITZ:25
.= 1. S by ;
hence p . k = 1_ S by
.= (rpoly (1,b)) . k by ;
:: thesis: verum
end;
end;
end;
hence rpoly (1,a) = rpoly (1,b) by ; :: thesis: verum