let f be PartFunc of REAL ,REAL ; :: thesis: for x0, g1 being Real holds
( f is_right_differentiable_in x0 & Rdiff f,x0 = g1 iff ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g1 ) ) ) )
let x0, g1 be Real; :: thesis: ( f is_right_differentiable_in x0 & Rdiff f,x0 = g1 iff ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g1 ) ) ) )
thus ( f is_right_differentiable_in x0 & Rdiff f,x0 = g1 implies ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g1 ) ) ) ) by Def3, Def6; :: thesis: ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g1 ) ) implies ( f is_right_differentiable_in x0 & Rdiff f,x0 = g1 ) )
assume that
A1: ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) and
A2: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g1 ) ; :: thesis: ( f is_right_differentiable_in x0 & Rdiff f,x0 = g1 )
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A2;
hence A3: f is_right_differentiable_in x0 by A1, Def3; :: thesis: Rdiff f,x0 = g1
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g1 by A2;
hence Rdiff f,x0 = g1 by A3, Def6; :: thesis: verum