let R be domRing; :: thesis: for a being Element of R
for i being Nat
for p being Element of the carrier of (Polynom-Ring R) holds ((a | R) *' p) . i = a * (p . i)
let a be Element of R; :: thesis: for i being Nat
for p being Element of the carrier of (Polynom-Ring R) holds ((a | R) *' p) . i = a * (p . i)
let i be Nat; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds ((a | R) *' p) . i = a * (p . i)
let p be Element of the carrier of (Polynom-Ring R); :: thesis: ((a | R) *' p) . i = a * (p . i)
reconsider p1 = p as Polynomial of R ;

per cases ( i = 0 or i <> 0 ) ;

suppose A1: i = 0 ; :: thesis: ((a | R) *' p) . i = a * (p . i)

then ((a | R) *' p1) . i = (<%a%> *' p1) . 0 by Lm3
.= (<%a,(0. R)%> *' p1) . 0 by POLYNOM5:43
.= a * (p1 . i) by A1, UPROOTS:37 ;
hence ((a | R) *' p) . i = a * (p . i) ; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: ((a | R) *' p) . i = a * (p . i)

then consider j being Nat such that
A3: i = j + 1 by NAT_1:6;
((a | R) *' p1) . i = (<%a%> *' p1) . (j + 1) by A3, Lm3
.= (<%a,(0. R)%> *' p1) . (j + 1) by POLYNOM5:43
.= (a * (p1 . (j + 1))) + ((0. R) * (p1 . j)) by UPROOTS:37
.= a * (p1 . (j + 1)) ;
hence ((a | R) *' p) . i = a * (p . i) by A3; :: thesis: verum

end;

end;