let F be Ring; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for a being Element of F holds (Deriv F) . (a * p) = a * ((Deriv F) . p)
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of F holds (Deriv F) . (a * p) = a * ((Deriv F) . p)
let a be Element of F; :: thesis: (Deriv F) . (a * p) = a * ((Deriv F) . p)
reconsider r = a * p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

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

let o be object ; :: thesis: ( o in NAT implies ((Deriv F) . r) . o = (a * ((Deriv F) . p)) . o )
assume o in NAT ; :: thesis: ((Deriv F) . r) . o = (a * ((Deriv F) . p)) . o
then reconsider i = o as Element of NAT ;
((Deriv F) . r) . i = (i + 1) * (r . (i + 1)) by RINGDER1:def 8
.= (i + 1) * (a * (p . (i + 1))) by POLYNOM5:def 4
.= ((i + 1) * a) * (p . (i + 1)) by BINOM:19
.= (a * (i + 1)) * (p . (i + 1)) by BINOM:17
.= a * ((i + 1) * (p . (i + 1))) by BINOM:21
.= a * (((Deriv F) . p) . i) by RINGDER1:def 8
.= (a * ((Deriv F) . p)) . i by POLYNOM5:def 4 ;
hence ((Deriv F) . r) . o = (a * ((Deriv F) . p)) . o ; :: thesis: verum

end;

hence (Deriv F) . (a * p) = a * ((Deriv F) . p) by FUNCT_2:12; :: thesis: verum