let L be non trivial right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative doubleLoopStr ; 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; for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
let x be Element of L; eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
defpred S1[ 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
S1[n] ) holds
S1[k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[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))
;
S1[k]
let p be
Polynomial of
L;
( len p = k implies eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) )
assume A3:
len p = k
;
eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
per cases
( len p <> 0 or len p = 0 )
;
suppose A4:
len p <> 0
;
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
;
verum end;
end;
A8:
for n being Nat holds S1[n]
from NAT_1:sch 4(A1);
len p = len p
;
hence
eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
by A8; verum