let R be Ring; :: thesis: for p being Polynomial of R
for a, b being Element of R holds (a * b) * p = a * (b * p)
let p be Polynomial of R; :: thesis: for a, b being Element of R holds (a * b) * p = a * (b * p)
let a, b be Element of R; :: thesis: (a * b) * p = a * (b * p)

now :: thesis: for o being object st o in NAT holds
((a * b) * p) . o = (a * (b * p)) . o

let o be object ; :: thesis: ( o in NAT implies ((a * b) * p) . o = (a * (b * p)) . o )
assume o in NAT ; :: thesis: ((a * b) * p) . o = (a * (b * p)) . o
then reconsider j = o as Element of NAT ;
thus ((a * b) * p) . o = (a * b) * (p . j) by POLYNOM5:def 4
.= a * (b * (p . j)) by GROUP_1:def 3
.= a * ((b * p) . j) by POLYNOM5:def 4
.= (a * (b * p)) . o by POLYNOM5:def 4 ; :: thesis: verum

end;

hence (a * b) * p = a * (b * p) ; :: thesis: verum