:: deftheorem defines is_right_differentiable_in FDIFF_3:def 3 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_right_differentiable_in x0 iff ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) );