:: The Limit of a Composition of Real Functions :: by Jaros{\l}aw Kotowicz :: :: Received September 5, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for g, r being Real st 0 < g holds ( r - g < r & r < r + g ) proofend; Lm2: for f2, f1 being PartFunc of REAL,REAL for s being Real_Sequence st rng s c= dom (f2 * f1) holds ( rng s c= dom f1 & rng (f1 /* s) c= dom f2 ) proofend; theorem Th1: :: LIMFUNC4:1 for f2, f1 being PartFunc of REAL,REAL for s being Real_Sequence for X being set st rng s c= (dom (f2 * f1)) /\ X holds ( rng s c= dom (f2 * f1) & rng s c= X & rng s c= dom f1 & rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 ) proofend; theorem Th2: :: LIMFUNC4:2 for f2, f1 being PartFunc of REAL,REAL for s being Real_Sequence for X being set st rng s c= (dom (f2 * f1)) \ X holds ( rng s c= dom (f2 * f1) & rng s c= dom f1 & rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 ) proofend; theorem :: LIMFUNC4:3 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC4:4 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC4:5 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC4:6 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC4:7 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC4:8 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC4:9 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC4:10 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) holds f2 * f1 is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC4:11 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) holds f2 * f1 is_left_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:12 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) holds f2 * f1 is_left_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:13 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) holds f2 * f1 is_left_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:14 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) holds f2 * f1 is_left_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:15 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) holds f2 * f1 is_right_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:16 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) holds f2 * f1 is_right_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:17 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) holds f2 * f1 is_right_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:18 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) holds f2 * f1 is_right_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:19 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_divergent_to+infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds f1 . r < lim_left (f1,x0) ) ) holds f2 * f1 is_left_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:20 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds f1 . r < lim_left (f1,x0) ) ) holds f2 * f1 is_left_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:21 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_right_divergent_to+infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds lim_left (f1,x0) < f1 . r ) ) holds f2 * f1 is_left_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:22 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_right_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds lim_left (f1,x0) < f1 . r ) ) holds f2 * f1 is_left_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:23 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_divergent_to+infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds lim_right (f1,x0) < f1 . r ) ) holds f2 * f1 is_right_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:24 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_divergent_to-infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds lim_right (f1,x0) < f1 . r ) ) holds f2 * f1 is_right_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:25 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_divergent_to+infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds f1 . r < lim_right (f1,x0) ) ) holds f2 * f1 is_right_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:26 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_divergent_to-infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds f1 . r < lim_right (f1,x0) ) ) holds f2 * f1 is_right_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:27 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_left_divergent_to+infty_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g < lim_in+infty f1 holds f2 * f1 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC4:28 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_left_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g < lim_in+infty f1 holds f2 * f1 is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC4:29 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_right_divergent_to+infty_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds lim_in+infty f1 < f1 . g holds f2 * f1 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC4:30 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_right_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds lim_in+infty f1 < f1 . g holds f2 * f1 is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC4:31 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_left_divergent_to+infty_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g < lim_in-infty f1 holds f2 * f1 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC4:32 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_left_divergent_to-infty_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g < lim_in-infty f1 holds f2 * f1 is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC4:33 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_right_divergent_to+infty_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds lim_in-infty f1 < f1 . g holds f2 * f1 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC4:34 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_right_divergent_to-infty_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds lim_in-infty f1 < f1 . g holds f2 * f1 is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC4:35 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds f2 * f1 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:36 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds f2 * f1 is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:37 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds f2 * f1 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:38 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds f2 * f1 is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:39 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_divergent_to+infty_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r <> lim (f1,x0) ) ) holds f2 * f1 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:40 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_divergent_to-infty_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r <> lim (f1,x0) ) ) holds f2 * f1 is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:41 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_right_divergent_to+infty_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r > lim (f1,x0) ) ) holds f2 * f1 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:42 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_right_divergent_to-infty_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r > lim (f1,x0) ) ) holds f2 * f1 is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:43 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_divergent_to+infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds f1 . r <> lim_right (f1,x0) ) ) holds f2 * f1 is_right_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:44 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_divergent_to-infty_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds f1 . r <> lim_right (f1,x0) ) ) holds f2 * f1 is_right_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:45 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_divergent_to+infty_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g <> lim_in+infty f1 holds f2 * f1 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC4:46 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_divergent_to-infty_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g <> lim_in+infty f1 holds f2 * f1 is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC4:47 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_divergent_to+infty_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g <> lim_in-infty f1 holds f2 * f1 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC4:48 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_divergent_to-infty_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g <> lim_in-infty f1 holds f2 * f1 is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC4:49 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_left_divergent_to+infty_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r < lim (f1,x0) ) ) holds f2 * f1 is_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:50 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_left_divergent_to-infty_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r < lim (f1,x0) ) ) holds f2 * f1 is_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:51 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_divergent_to+infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds f1 . r <> lim_left (f1,x0) ) ) holds f2 * f1 is_left_divergent_to+infty_in x0 proofend; theorem :: LIMFUNC4:52 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds f1 . r <> lim_left (f1,x0) ) ) holds f2 * f1 is_left_divergent_to-infty_in x0 proofend; theorem :: LIMFUNC4:53 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) holds ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_in+infty f2 ) proofend; theorem :: LIMFUNC4:54 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) holds ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_in-infty f2 ) proofend; theorem :: LIMFUNC4:55 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) holds ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_in+infty f2 ) proofend; theorem :: LIMFUNC4:56 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) holds ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_in-infty f2 ) proofend; theorem :: LIMFUNC4:57 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & f2 is convergent_in+infty & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) holds ( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_in+infty f2 ) proofend; theorem :: LIMFUNC4:58 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to-infty_in x0 & f2 is convergent_in-infty & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) holds ( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_in-infty f2 ) proofend; theorem :: LIMFUNC4:59 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to+infty_in x0 & f2 is convergent_in+infty & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) holds ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_in+infty f2 ) proofend; theorem :: LIMFUNC4:60 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is convergent_in-infty & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) holds ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_in-infty f2 ) proofend; theorem :: LIMFUNC4:61 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds f1 . r < lim_left (f1,x0) ) ) holds ( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_left (f2,(lim_left (f1,x0))) ) proofend; theorem :: LIMFUNC4:62 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds lim_right (f1,x0) < f1 . r ) ) holds ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_right (f2,(lim_right (f1,x0))) ) proofend; theorem :: LIMFUNC4:63 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_right_convergent_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds lim_left (f1,x0) < f1 . r ) ) holds ( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim_right (f2,(lim_left (f1,x0))) ) proofend; theorem :: LIMFUNC4:64 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_left_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds f1 . r < lim_right (f1,x0) ) ) holds ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim_left (f2,(lim_right (f1,x0))) ) proofend; theorem :: LIMFUNC4:65 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_left_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g < lim_in+infty f1 holds ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_left (f2,(lim_in+infty f1)) ) proofend; theorem :: LIMFUNC4:66 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_right_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds lim_in+infty f1 < f1 . g holds ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim_right (f2,(lim_in+infty f1)) ) proofend; theorem :: LIMFUNC4:67 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_left_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g < lim_in-infty f1 holds ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_left (f2,(lim_in-infty f1)) ) proofend; theorem :: LIMFUNC4:68 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_right_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds lim_in-infty f1 < f1 . g holds ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim_right (f2,(lim_in-infty f1)) ) proofend; theorem :: LIMFUNC4:69 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to+infty_in x0 & f2 is convergent_in+infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds ( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_in+infty f2 ) proofend; theorem :: LIMFUNC4:70 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is convergent_in-infty & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds ex g1, g2 being Real st ( r1 < g1 & g1 < x0 & g1 in dom (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) holds ( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_in-infty f2 ) proofend; theorem :: LIMFUNC4:71 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is_convergent_in lim_in+infty f1 & ( for r being Real ex g being Real st ( r < g & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g <> lim_in+infty f1 holds ( f2 * f1 is convergent_in+infty & lim_in+infty (f2 * f1) = lim (f2,(lim_in+infty f1)) ) proofend; theorem :: LIMFUNC4:72 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is_convergent_in lim_in-infty f1 & ( for r being Real ex g being Real st ( g < r & g in dom (f2 * f1) ) ) & ex r being Real st for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g <> lim_in-infty f1 holds ( f2 * f1 is convergent_in-infty & lim_in-infty (f2 * f1) = lim (f2,(lim_in-infty f1)) ) proofend; theorem :: LIMFUNC4:73 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_left_convergent_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r < lim (f1,x0) ) ) holds ( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_left (f2,(lim (f1,x0))) ) proofend; theorem :: LIMFUNC4:74 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_convergent_in lim_left (f1,x0) & ( for r being Real st r < x0 holds ex g being Real st ( r < g & g < x0 & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].(x0 - g),x0.[ holds f1 . r <> lim_left (f1,x0) ) ) holds ( f2 * f1 is_left_convergent_in x0 & lim_left ((f2 * f1),x0) = lim (f2,(lim_left (f1,x0))) ) proofend; theorem :: LIMFUNC4:75 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_right_convergent_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds lim (f1,x0) < f1 . r ) ) holds ( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim_right (f2,(lim (f1,x0))) ) proofend; theorem :: LIMFUNC4:76 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_convergent_in lim_right (f1,x0) & ( for r being Real st x0 < r holds ex g being Real st ( g < r & x0 < g & g in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ ].x0,(x0 + g).[ holds f1 . r <> lim_right (f1,x0) ) ) holds ( f2 * f1 is_right_convergent_in x0 & lim_right ((f2 * f1),x0) = lim (f2,(lim_right (f1,x0))) ) proofend; theorem :: LIMFUNC4:77 for x0 being Real for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in lim (f1,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 (f2 * f1) & g2 < r2 & x0 < g2 & g2 in dom (f2 * f1) ) ) & ex g being Real st ( 0 < g & ( for r being Real st r in (dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) holds f1 . r <> lim (f1,x0) ) ) holds ( f2 * f1 is_convergent_in x0 & lim ((f2 * f1),x0) = lim (f2,(lim (f1,x0))) ) proofend;