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

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

let o be object ; :: thesis: ( o in NAT implies ((a + b) * p) . o = ((a * p) + (b * p)) . o )
assume o in NAT ; :: thesis: ((a + b) * p) . o = ((a * p) + (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 * (p . j)) + (b * (p . j)) by VECTSP_1:def 3
.= ((a * p) . j) + (b * (p . j)) by POLYNOM5:def 4
.= ((a * p) . j) + ((b * p) . j) by POLYNOM5:def 4
.= ((a * p) + (b * p)) . o by NORMSP_1:def 2 ; :: thesis: verum

end;

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