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

A4: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A5: seq is convergent and
A6: lim seq = x0 and
A7: rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) ; :: thesis:
A8: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A7, Lm2;
A9: rng seq c= (dom f1) /\ (right_open_halfline x0) by A7, Lm2;
A10: rng seq c= (dom f2) /\ (right_open_halfline x0) by A7, Lm2;
then A11: lim (f2 /* seq) = lim_right (f2,x0) by A2, A5, A6, Def8;
A12: f2 /* seq is convergent by A2, A5, A6, A10;
rng seq c= dom (f1 (#) f2) by A7, Lm2;
then A13: (f1 /* seq) (#) (f2 /* seq) = (f1 (#) f2) /* seq by A8, RFUNCT_2:8;
A14: f1 /* seq is convergent by A1, A5, A6, A9;
hence (f1 (#) f2) /* seq is convergent by A12, A13; :: thesis:
lim (f1 /* seq) = lim_right (f1,x0) by A1, A5, A6, A9, Def8;
hence lim ((f1 (#) f2) /* seq) = (lim_right (f1,x0)) * (lim_right (f2,x0)) by A14, A12, A11, A13, SEQ_2:15; :: thesis:

end;

hence f1 (#) f2 is_right_convergent_in x0 by A3; :: thesis:
hence lim_right ((f1 (#) f2),x0) = (lim_right (f1,x0)) * (lim_right (f2,x0)) by A4, Def8; :: thesis: