let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) ) ) holds
( f1 + f2 is_left_convergent_in x0 & lim_left (f1 + f2),x0 = (lim_left f1,x0) + (lim_left f2,x0) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) ) ) implies ( f1 + f2 is_left_convergent_in x0 & lim_left (f1 + f2),x0 = (lim_left f1,x0) + (lim_left f2,x0) ) )
assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) ) ; :: thesis: ( f1 + f2 is_left_convergent_in x0 & lim_left (f1 + f2),x0 = (lim_left f1,x0) + (lim_left f2,x0) )

A4: now

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (left_open_halfline x0) implies ( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_left f1,x0) + (lim_left f2,x0) ) )
assume that
A5: seq is convergent and
A6: lim seq = x0 and
A7: rng seq c= (dom (f1 + f2)) /\ (left_open_halfline x0) ; :: thesis: ( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_left f1,x0) + (lim_left f2,x0) )
A8: dom (f1 + f2) = (dom f1) /\ (dom f2) by A7, Lm4;
A9: rng seq c= (dom f1) /\ (left_open_halfline x0) by A7, Lm4;
A10: rng seq c= (dom f2) /\ (left_open_halfline x0) by A7, Lm4;
then A11: lim (f2 /* seq) = lim_left f2,x0 by A2, A5, A6, Def7;
lim_left f2,x0 = lim_left f2,x0 ;
then A12: f2 /* seq is convergent by A2, A5, A6, A10, Def7;
rng seq c= dom (f1 + f2) by A7, Lm4;
then A13: (f1 /* seq) + (f2 /* seq) = (f1 + f2) /* seq by A8, RFUNCT_2:23;
lim_left f1,x0 = lim_left f1,x0 ;
then A14: f1 /* seq is convergent by A1, A5, A6, A9, Def7;
hence (f1 + f2) /* seq is convergent by A12, A13, SEQ_2:19; :: thesis: lim ((f1 + f2) /* seq) = (lim_left f1,x0) + (lim_left f2,x0)
lim (f1 /* seq) = lim_left f1,x0 by A1, A5, A6, A9, Def7;
hence lim ((f1 + f2) /* seq) = (lim_left f1,x0) + (lim_left f2,x0) by A14, A12, A11, A13, SEQ_2:20; :: thesis: verum

end;

hence f1 + f2 is_left_convergent_in x0 by A3, Def1; :: thesis: lim_left (f1 + f2),x0 = (lim_left f1,x0) + (lim_left f2,x0)
hence lim_left (f1 + f2),x0 = (lim_left f1,x0) + (lim_left f2,x0) by A4, Def7; :: thesis: verum