let L be non trivial right_complementable add-associative right_zeroed distributive left_unital associative commutative doubleLoopStr ; :: thesis: for p, q being Polynomial of L
for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))
let p, q be Polynomial of L; :: thesis: for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))
let x be Element of L; :: thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))
set p1 = (len p) -' 1;
set q1 = (len q) -' 1;

per cases ( ( len p <> 0 & len q <> 0 ) or len p = 0 or len q = 0 ) ;

suppose A1: ( len p <> 0 & len q <> 0 ) ; :: thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))

then A2: len q >= 0 + 1 by NAT_1:13;
then (len q) - 1 >= 0 by XREAL_1:19;
then A3: (len q) - 1 = (len q) -' 1 by XREAL_0:def 2;
A4: len p >= 0 + 1 by A1, NAT_1:13;
then (len p) - 1 >= 0 by XREAL_1:19;
then A5: (len p) - 1 = (len p) -' 1 by XREAL_0:def 2;
(len p) + (len q) >= 0 + (1 + 1) by A4, A2, XREAL_1:7;
then ((len p) + (len q)) - 2 >= 0 by XREAL_1:19;
then A6: ((len p) + (len q)) -' 2 = ((len p) + (len q)) - 2 by XREAL_0:def 2;
A7: ((len p) + (len q)) - (1 + 1) = ((len p) - 1) + ((len q) - 1) ;
set P1 = (power L) . (x,((len p) -' 1));
set Q1 = (power L) . (x,((len q) -' 1));
thus eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2))) by A1, Lm2
.= ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * (((power L) . (x,((len p) -' 1))) * ((power L) . (x,((len q) -' 1)))) by A5, A3, A6, A7, POLYNOM2:1
.= (p . ((len p) -' 1)) * ((q . ((len q) -' 1)) * (((power L) . (x,((len p) -' 1))) * ((power L) . (x,((len q) -' 1))))) by GROUP_1:def 3
.= (p . ((len p) -' 1)) * (((power L) . (x,((len p) -' 1))) * ((q . ((len q) -' 1)) * ((power L) . (x,((len q) -' 1))))) by GROUP_1:def 3
.= ((p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))) * ((q . ((len q) -' 1)) * ((power L) . (x,((len q) -' 1)))) by GROUP_1:def 3
.= ((p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))) * (eval ((Leading-Monomial q),x)) by Th22
.= (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) by Th22 ; :: thesis: verum

end;

suppose len p = 0 ; :: thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))

then A8: Leading-Monomial p = 0_. L by Th12;
hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = eval ((0_. L),x) by Th2
.= 0. L by Th17
.= (0. L) * (eval ((Leading-Monomial q),x))
.= (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) by A8, Th17 ;
:: thesis: verum

end;

suppose len q = 0 ; :: thesis: eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))

then len (Leading-Monomial q) = 0 by Th15;
then A9: Leading-Monomial q = 0_. L by Th5;
hence eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = eval ((0_. L),x) by POLYNOM3:34
.= 0. L by Th17
.= (eval ((Leading-Monomial p),x)) * (0. L)
.= (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x)) by A9, Th17 ;
:: thesis: verum

end;

end;