let r, x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( ( f is_divergent_to+infty_in x0 & r > 0 implies r (#) f is_divergent_to+infty_in x0 ) & ( f is_divergent_to+infty_in x0 & r < 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r > 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r < 0 implies r (#) f is_divergent_to+infty_in x0 ) )
let f be PartFunc of REAL,REAL; :: thesis: ( ( f is_divergent_to+infty_in x0 & r > 0 implies r (#) f is_divergent_to+infty_in x0 ) & ( f is_divergent_to+infty_in x0 & r < 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r > 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r < 0 implies r (#) f is_divergent_to+infty_in x0 ) )
thus ( f is_divergent_to+infty_in x0 & r > 0 implies r (#) f is_divergent_to+infty_in x0 ) :: thesis: ( ( f is_divergent_to+infty_in x0 & r < 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r > 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r < 0 implies r (#) f is_divergent_to+infty_in x0 ) )

proof

assume that
A1: f is_divergent_to+infty_in x0 and
A2: r > 0 ; :: thesis: r (#) 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 (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) :: according to LIMFUNC3:def 2 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} holds
(r (#) f) /* seq is divergent_to+infty

proof

let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) )
assume that
A3: r1 < x0 and
A4: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
consider g1, g2 being Real such that
A5: r1 < g1 and
A6: g1 < x0 and
A7: g1 in dom f and
A8: g2 < r2 and
A9: x0 < g2 and
A10: g2 in dom f by A1, A3, A4;
take g1 ; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
take g2 ; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
thus ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) by A5, A6, A7, A8, A9, A10, VALUED_1:def 5; :: thesis: verum

end;

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} implies (r (#) f) /* seq is divergent_to+infty )
assume that
A11: seq is convergent and
A12: lim seq = x0 and
A13: rng seq c= (dom (r (#) f)) \ {x0} ; :: thesis: (r (#) f) /* seq is divergent_to+infty
A14: rng seq c= (dom f) \ {x0} by A13, VALUED_1:def 5;
then f /* seq is divergent_to+infty by A1, A11, A12;
then r (#) (f /* seq) is divergent_to+infty by A2, LIMFUNC1:13;
hence (r (#) f) /* seq is divergent_to+infty by A14, RFUNCT_2:9, XBOOLE_1:1; :: thesis: verum

end;

thus ( f is_divergent_to+infty_in x0 & r < 0 implies r (#) f is_divergent_to-infty_in x0 ) :: thesis: ( ( f is_divergent_to-infty_in x0 & r > 0 implies r (#) f is_divergent_to-infty_in x0 ) & ( f is_divergent_to-infty_in x0 & r < 0 implies r (#) f is_divergent_to+infty_in x0 ) )

proof

assume that
A15: f is_divergent_to+infty_in x0 and
A16: r < 0 ; :: thesis: r (#) 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 (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) :: according to LIMFUNC3:def 3 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} holds
(r (#) f) /* seq is divergent_to-infty

proof

let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) )
assume that
A17: r1 < x0 and
A18: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
consider g1, g2 being Real such that
A19: r1 < g1 and
A20: g1 < x0 and
A21: g1 in dom f and
A22: g2 < r2 and
A23: x0 < g2 and
A24: g2 in dom f by A15, A17, A18;
take g1 ; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
take g2 ; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
thus ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) by A19, A20, A21, A22, A23, A24, VALUED_1:def 5; :: thesis: verum

end;

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} implies (r (#) f) /* seq is divergent_to-infty )
assume that
A25: seq is convergent and
A26: lim seq = x0 and
A27: rng seq c= (dom (r (#) f)) \ {x0} ; :: thesis: (r (#) f) /* seq is divergent_to-infty
A28: rng seq c= (dom f) \ {x0} by A27, VALUED_1:def 5;
then f /* seq is divergent_to+infty by A15, A25, A26;
then r (#) (f /* seq) is divergent_to-infty by A16, LIMFUNC1:13;
hence (r (#) f) /* seq is divergent_to-infty by A28, RFUNCT_2:9, XBOOLE_1:1; :: thesis: verum

end;

thus ( f is_divergent_to-infty_in x0 & r > 0 implies r (#) f is_divergent_to-infty_in x0 ) :: thesis: ( f is_divergent_to-infty_in x0 & r < 0 implies r (#) f is_divergent_to+infty_in x0 )

proof

assume that
A29: f is_divergent_to-infty_in x0 and
A30: r > 0 ; :: thesis: r (#) 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 (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) :: according to LIMFUNC3:def 3 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} holds
(r (#) f) /* seq is divergent_to-infty

proof

let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) )
assume that
A31: r1 < x0 and
A32: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
consider g1, g2 being Real such that
A33: r1 < g1 and
A34: g1 < x0 and
A35: g1 in dom f and
A36: g2 < r2 and
A37: x0 < g2 and
A38: g2 in dom f by A29, A31, A32;
take g1 ; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
take g2 ; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
thus ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) by A33, A34, A35, A36, A37, A38, VALUED_1:def 5; :: thesis: verum

end;

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} implies (r (#) f) /* seq is divergent_to-infty )
assume that
A39: seq is convergent and
A40: lim seq = x0 and
A41: rng seq c= (dom (r (#) f)) \ {x0} ; :: thesis: (r (#) f) /* seq is divergent_to-infty
A42: rng seq c= (dom f) \ {x0} by A41, VALUED_1:def 5;
then f /* seq is divergent_to-infty by A29, A39, A40;
then r (#) (f /* seq) is divergent_to-infty by A30, LIMFUNC1:14;
hence (r (#) f) /* seq is divergent_to-infty by A42, RFUNCT_2:9, XBOOLE_1:1; :: thesis: verum

end;

assume that
A43: f is_divergent_to-infty_in x0 and
A44: r < 0 ; :: thesis: r (#) 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 (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) :: according to LIMFUNC3:def 2 :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} holds
(r (#) f) /* seq is divergent_to+infty

proof

let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) )
assume that
A45: r1 < x0 and
A46: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
consider g1, g2 being Real such that
A47: r1 < g1 and
A48: g1 < x0 and
A49: g1 in dom f and
A50: g2 < r2 and
A51: x0 < g2 and
A52: g2 in dom f by A43, A45, A46;
take g1 ; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
take g2 ; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) )
thus ( r1 < g1 & g1 < x0 & g1 in dom (r (#) f) & g2 < r2 & x0 < g2 & g2 in dom (r (#) f) ) by A47, A48, A49, A50, A51, A52, VALUED_1:def 5; :: thesis: verum

end;

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) \ {x0} implies (r (#) f) /* seq is divergent_to+infty )
assume that
A53: seq is convergent and
A54: lim seq = x0 and
A55: rng seq c= (dom (r (#) f)) \ {x0} ; :: thesis: (r (#) f) /* seq is divergent_to+infty
A56: rng seq c= (dom f) \ {x0} by A55, VALUED_1:def 5;
then f /* seq is divergent_to-infty by A43, A53, A54;
then r (#) (f /* seq) is divergent_to+infty by A44, LIMFUNC1:14;
hence (r (#) f) /* seq is divergent_to+infty by A56, RFUNCT_2:9, XBOOLE_1:1; :: thesis: verum