let L be domRing; :: 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)) * (() . (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)) * (() . (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 reconsider v1 = v as non zero Element of L by STRUCT_0:def 12;
deg p = deg (v1 * p) by Th25;
then (len F1) - 1 = deg (v * p) by
.= (len F2) - 1 by ;
then A7: dom F1 = dom F2 by FINSEQ_3:29;
now :: thesis: for i being object st i in dom F1 holds
F2 /. i = v * (F1 /. i)
let i be object ; :: 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)) * (() . (x,(i1 -' 1))) = F1 . i by A3, A8
.= F1 /. i by ;
thus F2 /. i = F2 . i by
.= ((v * p) . (i1 -' 1)) * (() . (x,(i1 -' 1))) by A6, A7, A8
.= (v * (p . (i1 -' 1))) * (() . (x,(i1 -' 1))) by POLYNOM5:def 4
.= v * (F1 /. i) by ; :: thesis: verum
end;
then F2 = v * F1 by ;
hence eval ((v * p),x) = v * (eval (p,x)) by ; :: thesis: verum
end;
suppose A10: v = 0. L ; :: thesis: eval ((v * p),x) = v * (eval (p,x))
hence eval ((v * p),x) = eval ((0_. L),x) by POLYNOM5:26
.= v * (eval (p,x)) by ;
:: thesis: verum
end;
end;