let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
r1 <= f2 . g ) ) holds
f1 (#) f2 is_right_divergent_to+infty_in x0
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_right_divergent_to+infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & 0 < r1 & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
r1 <= f2 . g ) ) implies f1 (#) f2 is_right_divergent_to+infty_in x0 )
assume A1: ( f1 is_right_divergent_to+infty_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: ( for r, r1 being Real holds
( not 0 < r or not 0 < r1 or ex g being Real st
( g in (dom f2) /\ ].x0,(x0 + r).[ & not r1 <= f2 . g ) ) or f1 (#) f2 is_right_divergent_to+infty_in x0 )
given r, t being Real such that A2: ( 0 < r & 0 < t & ( for g being Real st g in (dom f2) /\ ].x0,(x0 + r).[ holds
t <= f2 . g ) ) ; :: thesis: f1 (#) f2 is_right_divergent_to+infty_in x0

now

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 divergent_to+infty )
assume A3: ( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) ) ; :: thesis: (f1 (#) f2) /* seq is divergent_to+infty
x0 < x0 + r by A2, Lm1;
then consider k being Element of NAT such that
A4: for n being Element of NAT st k <= n holds
seq . n < x0 + r by A3, Th2;
A5: ( seq ^\ k is convergent & lim (seq ^\ k) = x0 ) by A3, SEQ_4:33;
rng (seq ^\ k) c= rng seq by VALUED_0:21;
then rng (seq ^\ k) c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) by A3, XBOOLE_1:1;
then A6: ( rng (seq ^\ k) c= dom (f1 (#) f2) & rng (seq ^\ k) c= right_open_halfline x0 & dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng (seq ^\ k) c= dom f1 & rng (seq ^\ k) c= dom f2 & rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline x0) ) by Lm2;
then A7: f1 /* (seq ^\ k) is divergent_to+infty by A1, A5, Def5;
A8: rng seq c= dom (f1 (#) f2) by A3, Lm2;

now

thus 0 < t by A2; :: thesis: for n being Element of NAT holds t <= (f2 /* (seq ^\ k)) . n
let n be Element of NAT ; :: thesis: t <= (f2 /* (seq ^\ k)) . n
seq . (n + k) < x0 + r by A4, NAT_1:12;
then A9: (seq ^\ k) . n < x0 + r by NAT_1:def 3;
A10: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then (seq ^\ k) . n in right_open_halfline x0 by A6;
then (seq ^\ k) . n in { g1 where g1 is Real : x0 < g1 } by XXREAL_1:230;
then ex g being Real st
( g = (seq ^\ k) . n & x0 < g ) ;
then (seq ^\ k) . n in { g2 where g2 is Real : ( x0 < g2 & g2 < x0 + r ) } by A9;
then (seq ^\ k) . n in ].x0,(x0 + r).[ by RCOMP_1:def 2;
then (seq ^\ k) . n in (dom f2) /\ ].x0,(x0 + r).[ by A6, A10, XBOOLE_0:def 4;
then t <= f2 . ((seq ^\ k) . n) by A2;
hence t <= (f2 /* (seq ^\ k)) . n by A6, FUNCT_2:185; :: thesis: verum

end;

then A11: (f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k)) is divergent_to+infty by A7, LIMFUNC1:49;
(f1 /* (seq ^\ k)) (#) (f2 /* (seq ^\ k)) = (f1 (#) f2) /* (seq ^\ k) by A6, RFUNCT_2:23
.= ((f1 (#) f2) /* seq) ^\ k by A8, VALUED_0:27 ;
hence (f1 (#) f2) /* seq is divergent_to+infty by A11, LIMFUNC1:34; :: thesis: verum

end;

hence f1 (#) f2 is_right_divergent_to+infty_in x0 by A1, Def5; :: thesis: verum