let x0 be Real; :: thesis: for f, f1 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= f1 . g ) ) holds
f is_divergent_to-infty_in x0
let f, f1 be PartFunc of REAL,REAL; :: thesis: ( f1 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ex r being Real st
( 0 < r & (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= f1 . g ) ) implies f is_divergent_to-infty_in x0 )
assume that
A1: f1 is_divergent_to-infty_in x0 and
A2: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ; :: thesis: ( for r being Real holds
( not 0 < r or not (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) or ex g being Real st
( g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & not f . g <= f1 . g ) ) or f is_divergent_to-infty_in x0 )
given r being Real such that A3: 0 < r and
A4: (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) and
A5: for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g <= f1 . g ; :: thesis: f is_divergent_to-infty_in x0
thus for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A2; :: according to LIMFUNC3:def 3 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
f /* seq is divergent_to-infty
let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies f /* s is divergent_to-infty )
assume that
A6: s is convergent and
A7: lim s = x0 and
A8: rng s c= (dom f) \ {x0} ; :: thesis: f /* s is divergent_to-infty
consider k being Element of NAT such that
A9: for n being Element of NAT st k <= n holds
( x0 - r < s . n & s . n < x0 + r ) by A3, A6, A7, Th7;
A10: rng (s ^\ k) c= rng s by VALUED_0:21;
then A11: rng (s ^\ k) c= (dom f) \ {x0} by A8;

now :: thesis: for x being object st x in rng (s ^\ k) holds
x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[

let x be object ; :: thesis: ( x in rng (s ^\ k) implies x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ )
assume x in rng (s ^\ k) ; :: thesis: x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
then consider n being Element of NAT such that
A12: (s ^\ k) . n = x by FUNCT_2:113;
A13: k <= n + k by NAT_1:12;
then s . (n + k) < x0 + r by A9;
then A14: (s ^\ k) . n < x0 + r by NAT_1:def 3;
x0 - r < s . (n + k) by A9, A13;
then x0 - r < (s ^\ k) . n by NAT_1:def 3;
then (s ^\ k) . n in { g1 where g1 is Real : ( x0 - r < g1 & g1 < x0 + r ) } by A14;
then A15: (s ^\ k) . n in ].(x0 - r),(x0 + r).[ by RCOMP_1:def 2;
(s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then not (s ^\ k) . n in {x0} by A11, XBOOLE_0:def 5;
then (s ^\ k) . n in ].(x0 - r),(x0 + r).[ \ {x0} by A15, XBOOLE_0:def 5;
hence x in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by A3, A12, Th4; :: thesis: verum

end;

then A16: rng (s ^\ k) c= ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ ;
A17: rng s c= dom f by A8, XBOOLE_1:1;
then rng (s ^\ k) c= dom f by A10;
then A18: rng (s ^\ k) c= (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A16, XBOOLE_1:19;
then A19: rng (s ^\ k) c= (dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A4;

A20: now :: thesis: for n being Nat holds (f /* (s ^\ k)) . n <= (f1 /* (s ^\ k)) . n

let n be Nat; :: thesis: (f /* (s ^\ k)) . n <= (f1 /* (s ^\ k)) . n
A21: n in NAT by ORDINAL1:def 12;
(s ^\ k) . n in rng (s ^\ k) by VALUED_0:28;
then f . ((s ^\ k) . n) <= f1 . ((s ^\ k) . n) by A5, A18;
then (f /* (s ^\ k)) . n <= f1 . ((s ^\ k) . n) by A17, A10, FUNCT_2:108, XBOOLE_1:1, A21;
hence (f /* (s ^\ k)) . n <= (f1 /* (s ^\ k)) . n by A19, FUNCT_2:108, XBOOLE_1:18, A21; :: thesis: verum

end;

A22: rng (s ^\ k) c= dom f1 by A19, XBOOLE_1:18;

now :: thesis: for x being object st x in rng (s ^\ k) holds
x in (dom f1) \ {x0}

let x be object ; :: thesis: ( x in rng (s ^\ k) implies x in (dom f1) \ {x0} )
assume A23: x in rng (s ^\ k) ; :: thesis: x in (dom f1) \ {x0}
then not x in {x0} by A11, XBOOLE_0:def 5;
hence x in (dom f1) \ {x0} by A22, A23, XBOOLE_0:def 5; :: thesis: verum

end;

then A24: rng (s ^\ k) c= (dom f1) \ {x0} ;
lim (s ^\ k) = x0 by A6, A7, SEQ_4:20;
then f1 /* (s ^\ k) is divergent_to-infty by A1, A6, A24;
then f /* (s ^\ k) is divergent_to-infty by A20, LIMFUNC1:43;
then (f /* s) ^\ k is divergent_to-infty by A8, VALUED_0:27, XBOOLE_1:1;
hence f /* s is divergent_to-infty by LIMFUNC1:7; :: thesis: verum