let L be non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; for p being Polynomial of L
for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))
let p be Polynomial of L; for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))
let v, x be Element of L; eval ((v * p),x) = v * (eval (p,x))
consider F1 being FinSequence of the carrier of L such that
A1:
eval (p,x) = Sum F1
and
A2:
len F1 = len p
and
A3:
for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1)))
by POLYNOM4:def 2;
consider F2 being FinSequence of the carrier of L such that
A4:
eval ((v * p),x) = Sum F2
and
A5:
len F2 = len (v * p)
and
A6:
for n being Element of NAT st n in dom F2 holds
F2 . n = ((v * p) . (n -' 1)) * ((power L) . (x,(n -' 1)))
by POLYNOM4:def 2;
per cases
( v <> 0. L or v = 0. L )
;
suppose
v <> 0. L
;
eval ((v * p),x) = v * (eval (p,x))then
len F1 = len F2
by A2, A5, Th25;
then A7:
dom F1 = dom F2
by FINSEQ_3:29;
now for i being object st i in dom F1 holds
F2 /. i = v * (F1 /. i)let i be
object ;
( i in dom F1 implies F2 /. i = v * (F1 /. i) )assume A8:
i in dom F1
;
F2 /. i = v * (F1 /. i)then reconsider i1 =
i as
Element of
NAT ;
A9:
(p . (i1 -' 1)) * ((power L) . (x,(i1 -' 1))) =
F1 . i
by A3, A8
.=
F1 /. i
by A8, PARTFUN1:def 6
;
thus F2 /. i =
F2 . i
by A7, A8, PARTFUN1:def 6
.=
((v * p) . (i1 -' 1)) * ((power L) . (x,(i1 -' 1)))
by A6, A7, A8
.=
(v * (p . (i1 -' 1))) * ((power L) . (x,(i1 -' 1)))
by Def4
.=
v * (F1 /. i)
by A9, GROUP_1:def 3
;
verum end; then
F2 = v * F1
by A7, POLYNOM1:def 1;
hence
eval (
(v * p),
x)
= v * (eval (p,x))
by A1, A4, POLYNOM1:12;
verum end;