let R be Ring; :: thesis: for p being Polynomial of R
for a being Element of R holds a * p = (a | R) *' p
let p be Polynomial of R; :: thesis: for a being Element of R holds a * p = (a | R) *' p
let a be Element of R; :: thesis: a * p = (a | R) *' p
set q = (a | R) *' p;

A: now :: thesis: for x being object st x in dom (a * p) holds
(a * p) . x = ((a | R) *' p) . x

let x be object ; :: thesis: ( x in dom (a * p) implies (a * p) . x = ((a | R) *' p) . x )
assume x in dom (a * p) ; :: thesis: (a * p) . x = ((a | R) *' p) . x
then reconsider i = x as Element of NAT ;
consider F being FinSequence of the carrier of R such that
A1: ( len F = i + 1 & ((a | R) *' p) . i = Sum F & ( for k being Element of NAT st k in dom F holds
F . k = ((a | R) . (k -' 1)) * (p . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;

A2: now :: thesis: for k being Element of NAT st k in dom F & k <> 1 holds
F /. k = 0. R

let k be Element of NAT ; :: thesis: ( k in dom F & k <> 1 implies F /. k = 0. R )
assume A3: ( k in dom F & k <> 1 ) ; :: thesis: F /. k = 0. R
then k in Seg (i + 1) by A1, FINSEQ_1:def 3;
then ( 1 <= k & k <= i + 1 ) by FINSEQ_1:1;
then A6: k -' 1 = k - 1 by XREAL_1:233;
A4: k - 1 <> 0 by A3;
thus F /. k = F . k by A3, PARTFUN1:def 6
.= ((a | R) . (k -' 1)) * (p . ((i + 1) -' k)) by A1, A3
.= (0. R) * (p . ((i + 1) -' k)) by A6, A4, poly0
.= 0. R ; :: thesis: verum

end;

I: (i + 1) -' 1 = (i + 1) - 1 by NAT_1:11, XREAL_1:233;
1 <= i + 1 by NAT_1:11;
then 1 in Seg (i + 1) ;
then A3: 1 in dom F by A1, FINSEQ_1:def 3;
then A4: F . 1 = ((a | R) . (1 -' 1)) * (p . ((i + 1) -' 1)) by A1
.= ((a | R) . 0) * (p . ((i + 1) -' 1)) by NAT_2:8
.= a * (p . i) by I, poly0 ;
Sum F = F /. 1 by A2, A3, POLYNOM2:3
.= F . 1 by A3, PARTFUN1:def 6 ;
hence (a * p) . x = ((a | R) *' p) . x by A4, A1, POLYNOM5:def 4; :: thesis: verum

end;

dom (a * p) = NAT by FUNCT_2:def 1
.= dom ((a | R) *' p) by FUNCT_2:def 1 ;
hence a * p = (a | R) *' p by A; :: thesis: verum