let L be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: 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; :: thesis: for v, x being Element of L holds eval (v * p),x = v * (eval p,x)
let v, x be Element of L; :: thesis: 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
;
:: thesis: eval (v * p),x = v * (eval p,x)then
len F1 = len F2
by A2, A5, Th26;
then A7:
dom F1 = dom F2
by FINSEQ_3:31;
now let i be
set ;
:: thesis: ( i in dom F1 implies F2 /. i = v * (F1 /. i) )assume A8:
i in dom F1
;
:: thesis: 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 8
;
thus F2 /. i =
F2 . i
by A7, A8, PARTFUN1:def 8
.=
((v * p) . (i1 -' 1)) * ((power L) . x,(i1 -' 1))
by A6, A7, A8
.=
(v * (p . (i1 -' 1))) * ((power L) . x,(i1 -' 1))
by Def3
.=
v * (F1 /. i)
by A9, GROUP_1:def 4
;
:: thesis: verum end; then
F2 = v * F1
by A7, POLYNOM1:def 2;
hence
eval (v * p),
x = v * (eval p,x)
by A1, A4, POLYNOM1:28;
:: thesis: verum end;