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 ;

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

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;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

now :: thesis: for m being Nat st m is_at_least_length_of p holds

len (rpoly (1,b)) <= m

then A11:
len p = len (rpoly (1,b))
by A7, ALGSEQ_1:def 3, ALGSEQ_1:def 2;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 ;

end;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

hence
len (rpoly (1,b)) <= m
; :: thesis: verumassume
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;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

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

p . k = (rpoly (1,b)) . k

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

let k be Nat; :: thesis: ( k < len (rpoly (1,b)) implies p . b_{1} = (rpoly (1,b)) . b_{1} )

assume A12: k < len (rpoly (1,b)) ; :: thesis: p . b_{1} = (rpoly (1,b)) . b_{1}

(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;

end;assume A12: k < len (rpoly (1,b)) ; :: thesis: p . 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 )
;

end;

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

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;.= - (((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

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

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;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