let x0 be Real; 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; ( 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 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) )
; ( f1 (#) f2 is_right_convergent_in x0 & lim_right ((f1 (#) f2),x0) = (lim_right (f1,x0)) * (lim_right (f2,x0)) )
A4:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) holds
( (f1 (#) f2) /* seq is convergent & lim ((f1 (#) f2) /* seq) = (lim_right (f1,x0)) * (lim_right (f2,x0)) )let seq be
Real_Sequence;
( 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 that A5:
seq is
convergent
and A6:
lim seq = x0
and A7:
rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0)
;
( (f1 (#) f2) /* seq is convergent & lim ((f1 (#) f2) /* seq) = (lim_right (f1,x0)) * (lim_right (f2,x0)) )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;
lim ((f1 (#) f2) /* seq) = (lim_right (f1,x0)) * (lim_right (f2,x0))
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;
verum end;
hence
f1 (#) f2 is_right_convergent_in x0
by A3; 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 A4, Def8; verum