let A, B be Ring; :: thesis: for p being Polynomial of A
for x being Element of B st A is Subring of B holds
Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))
let p be Polynomial of A; :: thesis: for x being Element of B st A is Subring of B holds
Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))
let x be Element of B; :: thesis: ( A is Subring of B implies Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1))) )
assume A0: A is Subring of B ; :: thesis: Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))
set LMp = Leading-Monomial p;
consider F being FinSequence of B such that
A1: Ext_eval ((Leading-Monomial p),x) = Sum F and
A2: len F = len (Leading-Monomial p) and
A3: for n being Element of NAT st n in dom F holds
F . n = (In (((Leading-Monomial p) . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) by Def1;
A4: len F = len p by A2, POLYNOM4:15;

per cases ( len p > 0 or len p = 0 ) ;

suppose A5: len p > 0 ; :: thesis: Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))

then A7: len p >= 0 + 1 by NAT_1:13;
then A6: len p in dom F by A4, FINSEQ_3:25;

now :: thesis: for i being Element of NAT st i in dom F & i <> len p holds
F /. i = 0. B

A8: (len p) -' 1 = (len p) - 1 by A5, XREAL_0:def 2;
let i be Element of NAT ; :: thesis: ( i in dom F & i <> len p implies F /. i = 0. B )
assume that
A9: i in dom F and
A10: i <> len p ; :: thesis: F /. i = 0. B
i >= 0 + 1 by A9, FINSEQ_3:25;
then i -' 1 = i - 1 by XREAL_0:def 2;
then A11: i -' 1 <> (len p) -' 1 by A10, A8;
thus F /. i = F . i by A9, PARTFUN1:def 6
.= (In (((Leading-Monomial p) . (i -' 1)),B)) * ((power B) . (x,(i -' 1))) by A3, A9
.= (In ((0. A),B)) * ((power B) . (x,(i -' 1))) by A11, POLYNOM4:def 1
.= (0. B) * ((power B) . (x,(i -' 1))) by A0, Lm5
.= 0. B ; :: thesis: verum

end;

then Sum F = F /. (len p) by A4, A7, FINSEQ_3:25, POLYNOM2:3
.= F . (len p) by A6, PARTFUN1:def 6
.= (In (((Leading-Monomial p) . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1))) by A3, A7, A4, FINSEQ_3:25 ;
hence Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1))) by A1, POLYNOM4:def 1; :: thesis: verum

end;

suppose A12: len p = 0 ; :: thesis: Ext_eval ((Leading-Monomial p),x) = (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1)))

then A13: p = 0_. A by POLYNOM4:5;
Leading-Monomial p = 0_. A by A12, POLYNOM4:12;
hence Ext_eval ((Leading-Monomial p),x) = (0. B) * ((power B) . (x,((len p) -' 1))) by Th17
.= (In ((0. A),B)) * ((power B) . (x,((len p) -' 1))) by A0, Lm5
.= (In ((p . ((len p) -' 1)),B)) * ((power B) . (x,((len p) -' 1))) by A13, FUNCOP_1:7 ;
:: thesis: verum

end;

end;