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

A2: now

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

end;

A4: now

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) implies ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim_left f,x0) ) )
A5: lim_left f,x0 = lim_left f,x0 ;
assume A6: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ) ; :: thesis: ( (r (#) f) /* seq is convergent & lim ((r (#) f) /* seq) = r * (lim_left f,x0) )
then A7: rng seq c= (dom f) /\ (left_open_halfline x0) by VALUED_1:def 5;
then A8: ( f /* seq is convergent & lim (f /* seq) = lim_left f,x0 ) by A1, A5, A6, Def7;
then A9: r (#) (f /* seq) is convergent by SEQ_2:21;
A10: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
then A11: r (#) (f /* seq) = (r (#) f) /* seq by A7, RFUNCT_2:24, XBOOLE_1:1;
thus (r (#) f) /* seq is convergent by A7, A9, A10, RFUNCT_2:24, XBOOLE_1:1; :: thesis: lim ((r (#) f) /* seq) = r * (lim_left f,x0)
thus lim ((r (#) f) /* seq) = r * (lim_left f,x0) by A8, A11, SEQ_2:22; :: thesis: verum

end;

hence r (#) f is_left_convergent_in x0 by A2, Def1; :: thesis: lim_left (r (#) f),x0 = r * (lim_left f,x0)
hence lim_left (r (#) f),x0 = r * (lim_left f,x0) by A4, Def7; :: thesis: verum