let f be PartFunc of REAL , REAL ; :: thesis: for r being Real holds
( ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) & ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )
let r be Real; :: thesis: ( ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) & ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )
thus ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) :: thesis: ( ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )

proof

assume A1: ( f is divergent_in+infty_to+infty & r > 0 ) ; :: thesis: r (#) f is divergent_in+infty_to+infty

A2: now

let r1 be Real; :: thesis: ex g being Real st
( r1 < g & g in dom (r (#) f) )
consider g being Real such that
A3: ( r1 < g & g in dom f ) by A1, Def7;
take g = g; :: thesis: ( r1 < g & g in dom (r (#) f) )
thus ( r1 < g & g in dom (r (#) f) ) by A3, VALUED_1:def 5; :: thesis: verum

end;

now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (r (#) f) implies (r (#) f) /* seq is divergent_to+infty )
assume ( seq is divergent_to+infty & rng seq c= dom (r (#) f) ) ; :: thesis: (r (#) f) /* seq is divergent_to+infty
then A4: ( seq is divergent_to+infty & rng seq c= dom f ) by VALUED_1:def 5;
then f /* seq is divergent_to+infty by A1, Def7;
then r (#) (f /* seq) is divergent_to+infty by A1, Th40;
hence (r (#) f) /* seq is divergent_to+infty by A4, RFUNCT_2:24; :: thesis: verum

end;

hence r (#) f is divergent_in+infty_to+infty by A2, Def7; :: thesis: verum

end;

thus ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) :: thesis: ( ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )

proof

assume A5: ( f is divergent_in+infty_to+infty & r < 0 ) ; :: thesis: r (#) f is divergent_in+infty_to-infty

A6: now

let r1 be Real; :: thesis: ex g being Real st
( r1 < g & g in dom (r (#) f) )
consider g being Real such that
A7: ( r1 < g & g in dom f ) by A5, Def7;
take g = g; :: thesis: ( r1 < g & g in dom (r (#) f) )
thus ( r1 < g & g in dom (r (#) f) ) by A7, VALUED_1:def 5; :: thesis: verum

end;

now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (r (#) f) implies (r (#) f) /* seq is divergent_to-infty )
assume ( seq is divergent_to+infty & rng seq c= dom (r (#) f) ) ; :: thesis: (r (#) f) /* seq is divergent_to-infty
then A8: ( seq is divergent_to+infty & rng seq c= dom f ) by VALUED_1:def 5;
then f /* seq is divergent_to+infty by A5, Def7;
then r (#) (f /* seq) is divergent_to-infty by A5, Th40;
hence (r (#) f) /* seq is divergent_to-infty by A8, RFUNCT_2:24; :: thesis: verum

end;

hence r (#) f is divergent_in+infty_to-infty by A6, Def8; :: thesis: verum

end;

thus ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) :: thesis: ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty )

proof

assume A9: ( f is divergent_in+infty_to-infty & r > 0 ) ; :: thesis: r (#) f is divergent_in+infty_to-infty

A10: now

let r1 be Real; :: thesis: ex g being Real st
( r1 < g & g in dom (r (#) f) )
consider g being Real such that
A11: ( r1 < g & g in dom f ) by A9, Def8;
take g = g; :: thesis: ( r1 < g & g in dom (r (#) f) )
thus ( r1 < g & g in dom (r (#) f) ) by A11, VALUED_1:def 5; :: thesis: verum

end;

now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (r (#) f) implies (r (#) f) /* seq is divergent_to-infty )
assume ( seq is divergent_to+infty & rng seq c= dom (r (#) f) ) ; :: thesis: (r (#) f) /* seq is divergent_to-infty
then A12: ( seq is divergent_to+infty & rng seq c= dom f ) by VALUED_1:def 5;
then f /* seq is divergent_to-infty by A9, Def8;
then r (#) (f /* seq) is divergent_to-infty by A9, Th41;
hence (r (#) f) /* seq is divergent_to-infty by A12, RFUNCT_2:24; :: thesis: verum

end;

hence r (#) f is divergent_in+infty_to-infty by A10, Def8; :: thesis: verum

end;

assume A13: ( f is divergent_in+infty_to-infty & r < 0 ) ; :: thesis: r (#) f is divergent_in+infty_to+infty

A14: now

let r1 be Real; :: thesis: ex g being Real st
( r1 < g & g in dom (r (#) f) )
consider g being Real such that
A15: ( r1 < g & g in dom f ) by A13, Def8;
take g = g; :: thesis: ( r1 < g & g in dom (r (#) f) )
thus ( r1 < g & g in dom (r (#) f) ) by A15, VALUED_1:def 5; :: thesis: verum

end;

now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (r (#) f) implies (r (#) f) /* seq is divergent_to+infty )
assume ( seq is divergent_to+infty & rng seq c= dom (r (#) f) ) ; :: thesis: (r (#) f) /* seq is divergent_to+infty
then A16: ( seq is divergent_to+infty & rng seq c= dom f ) by VALUED_1:def 5;
then f /* seq is divergent_to-infty by A13, Def8;
then r (#) (f /* seq) is divergent_to+infty by A13, Th41;
hence (r (#) f) /* seq is divergent_to+infty by A16, RFUNCT_2:24; :: thesis: verum

end;

hence r (#) f is divergent_in+infty_to+infty by A14, Def7; :: thesis: verum