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)) * ((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;

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 )
;

end;

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 A2, HURWITZ:def 2

.= (len F2) - 1 by A5, HURWITZ:def 2 ;

then A7: dom F1 = dom F2 by FINSEQ_3:29;

hence eval ((v * p),x) = v * (eval (p,x)) by A1, A4, POLYNOM1:12; :: thesis: verum

end;deg p = deg (v1 * p) by Th25;

then (len F1) - 1 = deg (v * p) by A2, HURWITZ:def 2

.= (len F2) - 1 by A5, HURWITZ:def 2 ;

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)

then
F2 = v * F1
by A7, POLYNOM1:def 1;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)) * ((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 POLYNOM5:def 4

.= v * (F1 /. i) by A9, GROUP_1:def 3 ; :: thesis: verum

end;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 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 POLYNOM5:def 4

.= v * (F1 /. i) by A9, GROUP_1:def 3 ; :: thesis: verum

hence eval ((v * p),x) = v * (eval (p,x)) by A1, A4, POLYNOM1:12; :: thesis: verum

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 A10, POLYNOM4:17 ;

:: thesis: verum

end;.= v * (eval (p,x)) by A10, POLYNOM4:17 ;

:: thesis: verum