:: LIMFUNC4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for g, r being Real st 0 < g holds
( r - g < r & r < r + g )
proof end;

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 )
proof end;

theorem Th1: :: LIMFUNC4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th2: :: LIMFUNC4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: LIMFUNC4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: LIMFUNC4:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: LIMFUNC4:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;