:: L_HOSPIT semantic presentation

begin

theorem :: L_HOSPIT:1
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V30() real ext-real ) Real) & ( for r1, r2 being ( ( ) ( V30() real ext-real ) Real) st r1 : ( ( ) ( V30() real ext-real ) Real) < x0 : ( ( ) ( V30() real ext-real ) Real) & x0 : ( ( ) ( V30() real ext-real ) Real) < r2 : ( ( ) ( V30() real ext-real ) Real) holds
ex g1, g2 being ( ( ) ( V30() real ext-real ) Real) st
( r1 : ( ( ) ( V30() real ext-real ) Real) < g1 : ( ( ) ( V30() real ext-real ) Real) & g1 : ( ( ) ( V30() real ext-real ) Real) < x0 : ( ( ) ( V30() real ext-real ) Real) & g1 : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & g2 : ( ( ) ( V30() real ext-real ) Real) < r2 : ( ( ) ( V30() real ext-real ) Real) & x0 : ( ( ) ( V30() real ext-real ) Real) < g2 : ( ( ) ( V30() real ext-real ) Real) & g2 : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) ;

theorem :: L_HOSPIT:2
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0, t being ( ( ) ( V30() real ext-real ) Real) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_right_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) & lim_right (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = t : ( ( ) ( V30() real ext-real ) Real) iff ( ( for r being ( ( ) ( V30() real ext-real ) Real) st x0 : ( ( ) ( V30() real ext-real ) Real) < r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) holds
ex t being ( ( ) ( V30() real ext-real ) Real) st
( t : ( ( ) ( V30() real ext-real ) Real) < r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) & x0 : ( ( ) ( V30() real ext-real ) Real) < t : ( ( ) ( V30() real ext-real ) Real) & t : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for a being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) st a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) is convergent & lim a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = x0 : ( ( ) ( V30() real ext-real ) Real) & rng a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) /* a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) /* a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = t : ( ( ) ( V30() real ext-real ) Real) ) ) ) ) ;

theorem :: L_HOSPIT:3
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0, t being ( ( ) ( V30() real ext-real ) Real) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_left_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) & lim_left (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = t : ( ( ) ( V30() real ext-real ) Real) iff ( ( for r being ( ( ) ( V30() real ext-real ) Real) st r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) < x0 : ( ( ) ( V30() real ext-real ) Real) holds
ex t being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) < t : ( ( ) ( V30() real ext-real ) Real) & t : ( ( ) ( V30() real ext-real ) Real) < x0 : ( ( ) ( V30() real ext-real ) Real) & t : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for a being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) st a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) is convergent & lim a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = x0 : ( ( ) ( V30() real ext-real ) Real) & rng a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) /* a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) /* a : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() non empty total quasi_total V35() V36() V37() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = t : ( ( ) ( V30() real ext-real ) Real) ) ) ) ) ;

theorem :: L_HOSPIT:4
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st ex N being ( ( ) ( open V71() V72() V73() ) Neighbourhood of x0 : ( ( ) ( V30() real ext-real ) Real) ) st N : ( ( ) ( V30() real ext-real ) Real) \ {x0 : ( ( ) ( V30() real ext-real ) Real) } : ( ( ) ( non empty V71() V72() V73() ) set ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) holds
for r1, r2 being ( ( ) ( V30() real ext-real ) Real) st r1 : ( ( ) ( V30() real ext-real ) Real) < x0 : ( ( ) ( V30() real ext-real ) Real) & x0 : ( ( ) ( V30() real ext-real ) Real) < r2 : ( ( ) ( V30() real ext-real ) Real) holds
ex g1, g2 being ( ( ) ( V30() real ext-real ) Real) st
( r1 : ( ( ) ( V30() real ext-real ) Real) < g1 : ( ( ) ( V30() real ext-real ) Real) & g1 : ( ( ) ( V30() real ext-real ) Real) < x0 : ( ( ) ( V30() real ext-real ) Real) & g1 : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & g2 : ( ( ) ( V30() real ext-real ) Real) < r2 : ( ( ) ( V30() real ext-real ) Real) & x0 : ( ( ) ( V30() real ext-real ) Real) < g2 : ( ( ) ( V30() real ext-real ) Real) & g2 : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: L_HOSPIT:5
for f, g being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st ex N being ( ( ) ( open V71() V72() V73() ) Neighbourhood of x0 : ( ( ) ( V30() real ext-real ) Real) ) st
( N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) \ {x0 : ( ( ) ( V30() real ext-real ) Real) } : ( ( ) ( non empty V71() V72() V73() ) set ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_divergent_to+infty_in x0 : ( ( ) ( V30() real ext-real ) Real) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_divergent_to+infty_in x0 : ( ( ) ( V30() real ext-real ) Real) ;

theorem :: L_HOSPIT:6
for f, g being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st ex N being ( ( ) ( open V71() V72() V73() ) Neighbourhood of x0 : ( ( ) ( V30() real ext-real ) Real) ) st
( N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) \ {x0 : ( ( ) ( V30() real ext-real ) Real) } : ( ( ) ( non empty V71() V72() V73() ) set ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_divergent_to-infty_in x0 : ( ( ) ( V30() real ext-real ) Real) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_divergent_to-infty_in x0 : ( ( ) ( V30() real ext-real ) Real) ;

theorem :: L_HOSPIT:7
for f, g being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st x0 : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) /\ (dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & [.x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .] : ( ( ) ( closed V71() V72() V73() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & [.x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .] : ( ( ) ( closed V71() V72() V73() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & [.x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .] : ( ( ) ( closed V71() V72() V73() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V30() real ext-real ) Real) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V30() real ext-real ) Real) & (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_right_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_right_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & lim_right ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = lim_right (((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].x0 : ( ( ) ( V30() real ext-real ) Real) ,(x0 : ( ( ) ( V30() real ext-real ) Real) + r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ) ) ;

theorem :: L_HOSPIT:8
for f, g being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st x0 : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) /\ (dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & [.(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .] : ( ( ) ( closed V71() V72() V73() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & [.(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .] : ( ( ) ( closed V71() V72() V73() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & [.(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .] : ( ( ) ( closed V71() V72() V73() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V30() real ext-real ) Real) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V30() real ext-real ) Real) & (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_left_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_left_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & lim_left ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = lim_left (((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| ].(x0 : ( ( ) ( V30() real ext-real ) Real) - r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) .[ : ( ( ) ( open V71() V72() V73() V99() V100() V104() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ) ) ;

theorem :: L_HOSPIT:9
for f, g being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st ex N being ( ( ) ( open V71() V72() V73() ) Neighbourhood of x0 : ( ( ) ( V30() real ext-real ) Real) ) st
( N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) \ {x0 : ( ( ) ( V30() real ext-real ) Real) } : ( ( ) ( non empty V71() V72() V73() ) set ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) & ex N being ( ( ) ( open V71() V72() V73() ) Neighbourhood of x0 : ( ( ) ( V30() real ext-real ) Real) ) st lim ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = lim (((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ) ;

theorem :: L_HOSPIT:10
for f, g being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,)
for x0 being ( ( ) ( V30() real ext-real ) Real) st ex N being ( ( ) ( open V71() V72() V73() ) Neighbourhood of x0 : ( ( ) ( V30() real ext-real ) Real) ) st
( N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) \ {x0 : ( ( ) ( V30() real ext-real ) Real) } : ( ( ) ( non empty V71() V72() V73() ) set ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) c= dom (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) c= dom ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V71() V72() V73() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) . x0 : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real V71() V72() V73() V74() V75() V76() V77() V93() V94() V101() V104() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() V99() V101() ) Element of K19(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( ) set ) ) ) & (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) / (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) `| N : ( ( ) ( open V71() V72() V73() ) Neighbourhood of b3 : ( ( ) ( V30() real ext-real ) Real) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( ) ( V30() real ext-real ) Real) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) is_convergent_in x0 : ( ( ) ( V30() real ext-real ) Real) & lim ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) / g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) Element of K19(K20(REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ,REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) = (diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ,x0 : ( ( ) ( V30() real ext-real ) Real) )) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) / (diff (g : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V5( REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) V6() V35() V36() V37() ) PartFunc of ,) ,x0 : ( ( ) ( V30() real ext-real ) Real) )) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V51() V71() V72() V73() V77() V101() V102() V104() ) set ) ) ) ;