let F be non degenerated comRing; :: thesis: ( (Deriv F) . (1_. F) = 0_. F & (Deriv F) . (0_. F) = 0_. F )
reconsider r = 1_. F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
H: NAT --> (0. F) = 0_. F by POLYNOM3:def 7;

now :: thesis: for o being object st o in NAT holds
((Deriv F) . r) . o = (0_. F) . o

let o be object ; :: thesis: ( o in NAT implies ((Deriv F) . r) . o = (0_. F) . o )
assume o in NAT ; :: thesis: ((Deriv F) . r) . o = (0_. F) . o
then reconsider i = o as Element of NAT ;
((Deriv F) . r) . i = (i + 1) * ((1_. F) . (i + 1)) by RINGDER1:def 8
.= (i + 1) * (0. F) by POLYNOM3:30
.= (0_. F) . i by H ;
hence ((Deriv F) . r) . o = (0_. F) . o ; :: thesis: verum

end;

hence 0_. F = (Deriv F) . (1_. F) by FUNCT_2:12; :: thesis: (Deriv F) . (0_. F) = 0_. F
thus (Deriv F) . (0_. F) = (Deriv F) . (0. (Polynom-Ring F)) by POLYNOM3:def 10
.= 0_. F by POLYNOM3:def 10 ; :: thesis: verum