let x0, r be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_right_convergent_in x0 holds
( r (#) f is_right_convergent_in x0 & lim_right (r (#) f),x0 = r * (lim_right f,x0) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_right_convergent_in x0 implies ( r (#) f is_right_convergent_in x0 & lim_right (r (#) f),x0 = r * (lim_right f,x0) ) )
assume A1: f is_right_convergent_in x0 ; :: thesis: ( r (#) f is_right_convergent_in x0 & lim_right (r (#) f),x0 = r * (lim_right f,x0) )

A2: now

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (right_open_halfline x0) implies ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim_right f,x0) ) )
assume that
A3: seq is convergent and
A4: lim seq = x0 and
A5: rng seq c= (dom (r (#) f)) /\ (right_open_halfline x0) ; :: thesis: ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim_right f,x0) )
A6: rng seq c= (dom f) /\ (right_open_halfline x0) by A5, VALUED_1:def 5;
A7: (dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;
then A8: r (#) (f /* seq) = (r (#) f) /* seq by A6, RFUNCT_2:24, XBOOLE_1:1;
lim_right f,x0 = lim_right f,x0 ;
then A9: f /* seq is convergent by A1, A3, A4, A6, Def8;
then r (#) (f /* seq) is convergent by SEQ_2:21;
hence (r (#) f) /* seq is convergent by A6, A7, RFUNCT_2:24, XBOOLE_1:1; :: thesis: lim ((r (#) f) /* seq) = r * (lim_right f,x0)
lim (f /* seq) = lim_right f,x0 by A1, A3, A4, A6, Def8;
hence lim ((r (#) f) /* seq) = r * (lim_right f,x0) by A9, A8, SEQ_2:22; :: thesis: verum

end;

now

let r1 be Real; :: thesis: ( x0 < r1 implies ex g being Real st
( g < r1 & x0 < g & g in dom (r (#) f) ) )
assume x0 < r1 ; :: thesis: ex g being Real st
( g < r1 & x0 < g & g in dom (r (#) f) )
then consider g being Real such that
A10: g < r1 and
A11: x0 < g and
A12: g in dom f by A1, Def4;
take g = g; :: thesis: ( g < r1 & x0 < g & g in dom (r (#) f) )
thus ( g < r1 & x0 < g & g in dom (r (#) f) ) by A10, A11, A12, VALUED_1:def 5; :: thesis: verum

end;

hence r (#) f is_right_convergent_in x0 by A2, Def4; :: thesis: lim_right (r (#) f),x0 = r * (lim_right f,x0)
hence lim_right (r (#) f),x0 = r * (lim_right f,x0) by A2, Def8; :: thesis: verum