let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) holds
( f1 (#) f2 is_right_convergent_in x0 & lim_right (f1 (#) f2),x0 = (lim_right f1,x0) * (lim_right f2,x0) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) implies ( f1 (#) f2 is_right_convergent_in x0 & lim_right (f1 (#) f2),x0 = (lim_right f1,x0) * (lim_right f2,x0) ) )
assume A1: ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) ) ; :: thesis: ( f1 (#) f2 is_right_convergent_in x0 & lim_right (f1 (#) f2),x0 = (lim_right f1,x0) * (lim_right f2,x0) )

A2: now

A3: ( lim_right f1,x0 = lim_right f1,x0 & lim_right f2,x0 = lim_right f2,x0 ) ;
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) implies ( (f1 (#) f2) /* seq is convergent & lim ((f1 (#) f2) /* seq) = (lim_right f1,x0) * (lim_right f2,x0) ) )
assume A4: ( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) ) ; :: thesis: ( (f1 (#) f2) /* seq is convergent & lim ((f1 (#) f2) /* seq) = (lim_right f1,x0) * (lim_right f2,x0) )
then A5: ( rng seq c= dom (f1 (#) f2) & rng seq c= right_open_halfline x0 & dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ (right_open_halfline x0) & rng seq c= (dom f2) /\ (right_open_halfline x0) ) by Lm2;
then A6: ( f1 /* seq is convergent & lim (f1 /* seq) = lim_right f1,x0 ) by A1, A3, A4, Def8;
A7: ( f2 /* seq is convergent & lim (f2 /* seq) = lim_right f2,x0 ) by A1, A3, A4, A5, Def8;
A8: (f1 /* seq) (#) (f2 /* seq) = (f1 (#) f2) /* seq by A5, RFUNCT_2:23;
hence (f1 (#) f2) /* seq is convergent by A6, A7, SEQ_2:28; :: thesis: lim ((f1 (#) f2) /* seq) = (lim_right f1,x0) * (lim_right f2,x0)
thus lim ((f1 (#) f2) /* seq) = (lim_right f1,x0) * (lim_right f2,x0) by A6, A7, A8, SEQ_2:29; :: thesis: verum

end;

hence f1 (#) f2 is_right_convergent_in x0 by A1, Def4; :: thesis: lim_right (f1 (#) f2),x0 = (lim_right f1,x0) * (lim_right f2,x0)
hence lim_right (f1 (#) f2),x0 = (lim_right f1,x0) * (lim_right f2,x0) by A2, Def8; :: thesis: verum