let R be Ring; :: thesis: for S being RingExtension of R

for p being Element of the carrier of (Polynom-Ring R)

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R)

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let p be Element of the carrier of (Polynom-Ring R); :: thesis: for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let q be Element of the carrier of (Polynom-Ring S); :: thesis: for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let a be Element of S; :: thesis: ( p = q implies Ext_eval (p,a) = eval (q,a) )

assume A1: p = q ; :: thesis: Ext_eval (p,a) = eval (q,a)

A2: R is Subring of S by Def1;

for p being Element of the carrier of (Polynom-Ring R)

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R)

for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let p be Element of the carrier of (Polynom-Ring R); :: thesis: for q being Element of the carrier of (Polynom-Ring S)

for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let q be Element of the carrier of (Polynom-Ring S); :: thesis: for a being Element of S st p = q holds

Ext_eval (p,a) = eval (q,a)

let a be Element of S; :: thesis: ( p = q implies Ext_eval (p,a) = eval (q,a) )

assume A1: p = q ; :: thesis: Ext_eval (p,a) = eval (q,a)

A2: R is Subring of S by Def1;

per cases
( q is zero or not q is zero )
;

end;

suppose
q is zero
; :: thesis: Ext_eval (p,a) = eval (q,a)

then A3:
q = 0_. S
by UPROOTS:def 5;

p = 0. (Polynom-Ring S) by A1, A3, POLYNOM3:def 10

.= 0. (Polynom-Ring R) by Th7

.= 0_. R by POLYNOM3:def 10 ;

hence Ext_eval (p,a) = 0. S by ALGNUM_1:13

.= eval (q,a) by A3, POLYNOM4:17 ;

:: thesis: verum

end;p = 0. (Polynom-Ring S) by A1, A3, POLYNOM3:def 10

.= 0. (Polynom-Ring R) by Th7

.= 0_. R by POLYNOM3:def 10 ;

hence Ext_eval (p,a) = 0. S by ALGNUM_1:13

.= eval (q,a) by A3, POLYNOM4:17 ;

:: thesis: verum

suppose A4:
not q is zero
; :: thesis: Ext_eval (p,a) = eval (q,a)

then
len q > 0
by UPROOTS:17;

then A5: (len q) -' 1 = (len q) - 1 by XREAL_0:def 2;

then reconsider lenq = (len q) - 1 as Element of NAT ;

consider Fp being FinSequence of S such that

A6: ( Ext_eval (p,a) = Sum Fp & len Fp = len p & ( for n being Element of NAT st n in dom Fp holds

Fp . n = (In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;

consider Fq being FinSequence of the carrier of S such that

A7: ( eval (q,a) = Sum Fq & len Fq = len q & ( for n being Element of NAT st n in dom Fq holds

Fq . n = (q . (n -' 1)) * ((power S) . (a,(n -' 1))) ) ) by POLYNOM4:def 2;

then A11: dom Fq = Seg (len p) by A7, FINSEQ_1:def 3

.= dom Fp by A6, FINSEQ_1:def 3 ;

for n being Nat st n in dom Fp holds

Fq . n = Fp . n

end;then A5: (len q) -' 1 = (len q) - 1 by XREAL_0:def 2;

then reconsider lenq = (len q) - 1 as Element of NAT ;

consider Fp being FinSequence of S such that

A6: ( Ext_eval (p,a) = Sum Fp & len Fp = len p & ( for n being Element of NAT st n in dom Fp holds

Fp . n = (In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;

consider Fq being FinSequence of the carrier of S such that

A7: ( eval (q,a) = Sum Fq & len Fq = len q & ( for n being Element of NAT st n in dom Fq holds

Fq . n = (q . (n -' 1)) * ((power S) . (a,(n -' 1))) ) ) by POLYNOM4:def 2;

A8: now :: thesis: for i being Nat st i >= len q holds

p . i = 0. R

p . i = 0. R

let i be Nat; :: thesis: ( i >= len q implies p . i = 0. R )

assume i >= len q ; :: thesis: p . i = 0. R

then q . i = 0. S by ALGSEQ_1:8;

hence p . i = 0. R by A1, A2, C0SP1:def 3; :: thesis: verum

end;assume i >= len q ; :: thesis: p . i = 0. R

then q . i = 0. S by ALGSEQ_1:8;

hence p . i = 0. R by A1, A2, C0SP1:def 3; :: thesis: verum

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

len q <= m

then
len p = len q
by A8, ALGSEQ_1:def 3, ALGSEQ_1:def 2;len q <= m

let m be Nat; :: thesis: ( m is_at_least_length_of p implies len q <= m )

assume A9: m is_at_least_length_of p ; :: thesis: len q <= m

end;assume A9: m is_at_least_length_of p ; :: thesis: len q <= m

now :: thesis: not len q > m

hence
len q <= m
; :: thesis: verumassume
len q > m
; :: thesis: contradiction

then lenq + 1 > m ;

then lenq >= m by NAT_1:13;

then p . ((len q) -' 1) = 0. R by A5, A9, ALGSEQ_1:def 2;

then A10: q . ((len q) -' 1) = 0. S by A1, A2, C0SP1:def 3;

0 + 1 < (len q) + 1 by A4, XREAL_1:8, UPROOTS:17;

then len q >= 1 by NAT_1:13;

then ((len q) -' 1) + 1 = len q by XREAL_1:235;

hence contradiction by A10, ALGSEQ_1:10; :: thesis: verum

end;then lenq + 1 > m ;

then lenq >= m by NAT_1:13;

then p . ((len q) -' 1) = 0. R by A5, A9, ALGSEQ_1:def 2;

then A10: q . ((len q) -' 1) = 0. S by A1, A2, C0SP1:def 3;

0 + 1 < (len q) + 1 by A4, XREAL_1:8, UPROOTS:17;

then len q >= 1 by NAT_1:13;

then ((len q) -' 1) + 1 = len q by XREAL_1:235;

hence contradiction by A10, ALGSEQ_1:10; :: thesis: verum

then A11: dom Fq = Seg (len p) by A7, FINSEQ_1:def 3

.= dom Fp by A6, FINSEQ_1:def 3 ;

for n being Nat st n in dom Fp holds

Fq . n = Fp . n

proof

hence
Ext_eval (p,a) = eval (q,a)
by A6, A7, A11, FINSEQ_1:13; :: thesis: verum
let n be Nat; :: thesis: ( n in dom Fp implies Fq . n = Fp . n )

assume A12: n in dom Fp ; :: thesis: Fq . n = Fp . n

hence Fp . n = (In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) by A6

.= (q . (n -' 1)) * ((power S) . (a,(n -' 1))) by A1

.= Fq . n by A7, A11, A12 ;

:: thesis: verum

end;assume A12: n in dom Fp ; :: thesis: Fq . n = Fp . n

hence Fp . n = (In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) by A6

.= (q . (n -' 1)) * ((power S) . (a,(n -' 1))) by A1

.= Fq . n by A7, A11, A12 ;

:: thesis: verum