let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of ()
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 ()
for q being Element of the carrier of ()
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 (); :: thesis: for q being Element of the carrier of ()
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 (); :: 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 ) ;
suppose q is zero ; :: thesis: Ext_eval (p,a) = eval (q,a)
then A3: q = 0_. S by UPROOTS:def 5;
p = 0. () by
.= 0. () by Th7
.= 0_. R by POLYNOM3:def 10 ;
hence Ext_eval (p,a) = 0. S by ALGNUM_1:13
.= eval (q,a) by ;
:: thesis: verum
end;
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)) * (() . (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)) * (() . (a,(n -' 1))) ) ) by POLYNOM4:def 2;
A8: now :: thesis: for i being Nat st i >= len q holds
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 ; :: thesis: verum
end;
now :: thesis: for m being Nat st m is_at_least_length_of p holds
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
now :: thesis: not len q > m
assume len q > m ; :: thesis: contradiction
then lenq + 1 > m ;
then lenq >= m by NAT_1:13;
then p . ((len q) -' 1) = 0. R by ;
then A10: q . ((len q) -' 1) = 0. S by ;
0 + 1 < (len q) + 1 by ;
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;
hence len q <= m ; :: thesis: verum
end;
then len p = len q by ;
then A11: dom Fq = Seg (len p) by
.= dom Fp by ;
for n being Nat st n in dom Fp holds
Fq . n = Fp . n
proof
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)) * (() . (a,(n -' 1))) by A6
.= (q . (n -' 1)) * (() . (a,(n -' 1))) by A1
.= Fq . n by A7, A11, A12 ;
:: thesis: verum
end;
hence Ext_eval (p,a) = eval (q,a) by ; :: thesis: verum
end;
end;