let F be Ring; :: thesis: for a being Element of F holds (Deriv F) . (X- a) = 1_. F
let a be Element of F; :: thesis: (Deriv F) . (X- a) = 1_. F
set p = 1_. F;
set q = (Deriv F) . (X- a);

now :: thesis: for o being object st o in NAT holds
(1_. F) . o = ((Deriv F) . (X- a)) . o

let o be object ; :: thesis: ( o in NAT implies (1_. F) . b₁ = ((Deriv F) . (X- a)) . b₁ )
assume o in NAT ; :: thesis: (1_. F) . b₁ = ((Deriv F) . (X- a)) . b₁
then reconsider i = o as Element of NAT ;

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

suppose A: i = 0 ; :: thesis: (1_. F) . b₁ = ((Deriv F) . (X- a)) . b₁

then ((Deriv F) . (X- a)) . i = (0 + 1) * ((X- a) . (0 + 1)) by RINGDER1:def 8
.= (X- a) . 1 by BINOM:13
.= (rpoly (1,a)) . 1 by FIELD_9:def 2
.= 1_ F by HURWITZ:25
.= (1_. F) . i by A, POLYNOM3:30 ;
hence (1_. F) . o = ((Deriv F) . (X- a)) . o ; :: thesis: verum

end;

suppose A: i <> 0 ; :: thesis: (1_. F) . b₁ = ((Deriv F) . (X- a)) . b₁

then B: i + 1 <> 1 ;
((Deriv F) . (X- a)) . i = (i + 1) * ((X- a) . (i + 1)) by RINGDER1:def 8
.= (i + 1) * ((rpoly (1,a)) . (i + 1)) by FIELD_9:def 2
.= (i + 1) * (0. F) by B, HURWITZ:26
.= (1_. F) . i by A, POLYNOM3:30 ;
hence (1_. F) . o = ((Deriv F) . (X- a)) . o ; :: thesis: verum

end;

end;

end;

hence (Deriv F) . (X- a) = 1_. F by FUNCT_2:12; :: thesis: verum