let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))
let p be Polynomial of L; :: thesis: for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))
let x be Element of L; :: thesis: eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))
set LMp = Leading-Monomial p;
consider F being FinSequence of the carrier of L such that
A1: 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 = ((Leading-Monomial p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2;
A4: len F = len p by A2, Th15;

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

suppose len p > 0 ; :: thesis: eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))

then A5: len p >= 0 + 1 by NAT_1:13;
then len p in Seg (len F) by A4, FINSEQ_1:1;
then A6: len p in dom F by FINSEQ_1:def 3;
A7: (len p) - 1 >= 0 by A5, XREAL_1:19;

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

A8: (len p) -' 1 = (len p) - 1 by A7, XREAL_0:def 2;
let i be Element of NAT ; :: thesis: ( i in dom F & i <> len p implies F /. i = 0. L )
assume that
A9: i in dom F and
A10: i <> len p ; :: thesis: F /. i = 0. L
i in Seg (len F) by A9, FINSEQ_1:def 3;
then i >= 0 + 1 by FINSEQ_1:1;
then i - 1 >= 0 by XREAL_1:19;
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
.= ((Leading-Monomial p) . (i -' 1)) * ((power L) . (x,(i -' 1))) by A3, A9
.= (0. L) * ((power L) . (x,(i -' 1))) by A11, Def1
.= 0. L ; :: thesis: verum

end;

then Sum F = F /. (len p) by A6, POLYNOM2:3
.= F . (len p) by A6, PARTFUN1:def 6
.= ((Leading-Monomial p) . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by A3, A6 ;
hence eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by A1, Def1; :: thesis: verum

end;

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

then A13: p = 0_. L by Th5;
Leading-Monomial p = 0_. L by A12, Th12;
hence eval ((Leading-Monomial p),x) = 0. L by Th17
.= (0. L) * ((power L) . (x,((len p) -' 1)))
.= (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1))) by A13, FUNCOP_1:7 ;
:: thesis: verum

end;

end;