let L be non empty right_complementable add-associative right_zeroed unital distributive 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, Th18;

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:3;
then A6: len p in dom F by FINSEQ_1:def 3;
A7: (len p) - 1 >= 0 by A5, XREAL_1:21;

now

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

end;

then Sum F = F /. (len p) by A6, POLYNOM2:5
.= F . (len p) by A6, PARTFUN1:def 8
.= ((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 A11: len p = 0 ; :: thesis: eval (Leading-Monomial p),x = (p . ((len p) -' 1)) * ((power L) . x,((len p) -' 1))

then A12: p = 0_. L by Th8;
Leading-Monomial p = 0_. L by A11, Th15;
hence eval (Leading-Monomial p),x = 0. L by Th20
.= (0. L) * ((power L) . x,((len p) -' 1)) by VECTSP_1:39
.= (p . ((len p) -' 1)) * ((power L) . x,((len p) -' 1)) by A12, FUNCOP_1:13 ;
:: thesis: verum

end;

end;