let L be non trivial right_complementable Abelian 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 ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let p, q be Polynomial of L; :: thesis: for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let x be Element of L; :: thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
defpred S₁[ Nat] means for p being Polynomial of L st len p = $1 holds
eval ((p *' q),x) = (eval (p,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 p being Polynomial of L st len p = n holds
eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) ; :: thesis: S₁[k]
let p be Polynomial of L; :: thesis: ( len p = k implies eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) )
assume A3: len p = k ; :: thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

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

suppose A4: len p <> 0 ; :: thesis: eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

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

end;

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

then A7: p = 0_. L by Th5;
hence eval ((p *' q),x) = eval ((0_. L),x) by Th2
.= 0. L by Th17
.= (0. L) * (eval (q,x))
.= (eval (p,x)) * (eval (q,x)) by A7, Th17 ;
:: thesis: verum

end;

end;

end;

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