let f be PartFunc of REAL,REAL; :: thesis: for x0, r being Real st r <> 0 & f is_right_differentiable_in x0 holds
( r (#) f is_right_differentiable_in x0 & Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) )
let x0, r be Real; :: thesis: ( r <> 0 & f is_right_differentiable_in x0 implies ( r (#) f is_right_differentiable_in x0 & Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) ) )
assume that
A1: r <> 0 and
A2: f is_right_differentiable_in x0 ; :: thesis: ( r (#) f is_right_differentiable_in x0 & Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) )
set v = |.r.|;
A3: |.r.| > 0 by A1, COMPLEX1:47;
A4: dom f = dom (r (#) f) by VALUED_1:def 5;
then A5: ex e being Real st
( e > 0 & [.x0,(x0 + e).] c= dom (r (#) f) ) by A2, FDIFF_3:def 3;
consider e being Real such that
A6: ( e > 0 & [.x0,(x0 + e).] c= dom f ) by A2, FDIFF_3:def 3;
A7: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (r (#) f) & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) is convergent & lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0)) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (r (#) f) & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) is convergent & lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0)) )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (r (#) f) & ( for n being Nat holds h . n > 0 ) implies ( (h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) is convergent & lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0)) ) )
assume that
A8: rng c = {x0} and
A9: rng (h + c) c= dom (r (#) f) and
A10: for n being Nat holds h . n > 0 ; :: thesis: ( (h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) is convergent & lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0)) )
A11: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A2, A4, A8, A9, A10, FDIFF_3:def 3;
A12: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Rdiff (f,x0) by A2, A4, A8, A9, A10, FDIFF_3:15;
A13: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p
then p / |.r.| > 0 by A3, XREAL_1:139;
then consider n being Nat such that
A14: for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Rdiff (f,x0))).| < p / |.r.| by A11, A12, SEQ_2:def 7;
take n ; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p
thus for m being Nat st n <= m holds
|.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p :: thesis: verum

proof

let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p )
assume n <= m ; :: thesis: |.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p
then |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Rdiff (f,x0))).| < p / |.r.| by A14;
then A15: |.r.| * |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Rdiff (f,x0))).| < p by A1, COMPLEX1:47, XREAL_1:79;
A16: |.r.| * |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Rdiff (f,x0))).| = |.(r * ((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Rdiff (f,x0)))).| by COMPLEX1:65
.= |.((r * (((h ") (#) ((f /* (h + c)) - (f /* c))) . m)) - (r * (Rdiff (f,x0)))).| ;
A17: dom (r (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = NAT by FUNCT_2:def 1;
x0 < x0 + e by A6, XREAL_1:29;
then x0 in [.x0,(x0 + e).] by XXREAL_1:1;
then ( rng (h + c) c= dom f & rng c c= dom f ) by A8, A9, A6, VALUED_1:def 5, ZFMISC_1:31;
then A18: ( r (#) (f /* (h + c)) = (r (#) f) /* (h + c) & r (#) (f /* c) = (r (#) f) /* c ) by RFUNCT_2:9;
r (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (h ") (#) (r (#) ((f /* (h + c)) - (f /* c))) by RFUNCT_1:13
.= (h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) by A18, RFUNCT_1:18 ;
hence |.((((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) . m) - (r * (Rdiff (f,x0)))).| < p by A15, A16, A17, ORDINAL1:def 12, VALUED_1:def 5; :: thesis: verum

end;

end;

hence (h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0))
hence lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0)) by A13, SEQ_2:def 7; :: thesis: verum

end;

then for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (r (#) f) & ( for n being Nat holds h . n > 0 ) holds
(h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c)) is convergent ;
hence A19: r (#) f is_right_differentiable_in x0 by A5, FDIFF_3:def 3; :: thesis: Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0))
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (r (#) f) & ( for n being Nat holds h . n > 0 ) holds
lim ((h ") (#) (((r (#) f) /* (h + c)) - ((r (#) f) /* c))) = r * (Rdiff (f,x0)) by A7;
hence Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) by A19, FDIFF_3:def 6; :: thesis: verum