let L be non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ; :: thesis: for p, q being Polynomial of L
for x being Element of L holds eval ((Leading-Monomial p) *' q),x = (eval (Leading-Monomial p),x) * (eval q,x)
let p1, q be Polynomial of L; :: thesis: for x being Element of L holds eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x)
let x be Element of L; :: thesis: eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x)
set p = Leading-Monomial p1;
defpred S₁[ Nat] means for q being Polynomial of L st len q = $1 holds
eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x);
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
for q being Polynomial of L st len q = n holds
eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x) ; :: thesis: S₁[k]
let q be Polynomial of L; :: thesis: ( len q = k implies eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x) )
assume A3: len q = k ; :: thesis: eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x)

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

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

then consider r being Polynomial of L such that
A4: len r < len q and
A5: q = r + (Leading-Monomial q) and
for n being Element of NAT st n < (len q) - 1 holds
r . n = q . n by Th19;
set LMq = Leading-Monomial q;
thus eval ((Leading-Monomial p1) *' q),x = eval (((Leading-Monomial p1) *' r) + ((Leading-Monomial p1) *' (Leading-Monomial q))),x by A5, POLYNOM3:32
.= (eval ((Leading-Monomial p1) *' r),x) + (eval ((Leading-Monomial p1) *' (Leading-Monomial q)),x) by Th22
.= ((eval (Leading-Monomial p1),x) * (eval r,x)) + (eval ((Leading-Monomial p1) *' (Leading-Monomial q)),x) by A2, A3, A4
.= ((eval (Leading-Monomial p1),x) * (eval r,x)) + ((eval (Leading-Monomial p1),x) * (eval (Leading-Monomial q),x)) by Lm4
.= (eval (Leading-Monomial p1),x) * ((eval r,x) + (eval (Leading-Monomial q),x)) by VECTSP_1:def 18
.= (eval (Leading-Monomial p1),x) * (eval q,x) by A5, Th22 ; :: thesis: verum

end;

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

then A6: q = 0_. L by Th8;
hence eval ((Leading-Monomial p1) *' q),x = eval (0_. L),x by POLYNOM3:35
.= 0. L by Th20
.= (eval (Leading-Monomial p1),x) * (0. L) by VECTSP_1:39
.= (eval (Leading-Monomial p1),x) * (eval q,x) by A6, Th20 ;
:: thesis: verum

end;

end;

end;

A7: len q = len q ;
for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
hence eval ((Leading-Monomial p1) *' q),x = (eval (Leading-Monomial p1),x) * (eval q,x) by A7; :: thesis: verum