LIMFUNC1

:: LIMFUNC1 semantic presentation

begin

notation

let r be ( ( real ) ( V30() real ext-real ) number ) ;
synonym left_open_halfline r for halfline r;

end;

definition

let r be ( ( real ) ( V30() real ext-real ) number ) ;

func left_closed_halfline r -> ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) equals :: LIMFUNC1:def 1
].-infty : ( ( ) ( non empty non real ext-real non positive negative ) set ) ,r : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) .] : ( ( ) ( ) set ) ;

func right_closed_halfline r -> ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) equals :: LIMFUNC1:def 2
[.r : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( ) set ) ;

func right_open_halfline r -> ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) equals :: LIMFUNC1:def 3
].r : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) ,+infty : ( ( ) ( non empty non real ext-real positive non negative ) set ) .[ : ( ( ) ( ) set ) ;

end;

theorem :: LIMFUNC1:1

theorem :: LIMFUNC1:2

theorem :: LIMFUNC1:3

theorem :: LIMFUNC1:4

theorem :: LIMFUNC1:5

definition

let seq be ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ;

attr seq is divergent_to+infty means :: LIMFUNC1:def 4
for r being ( ( ) ( V30() real ext-real ) Real) ex n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) st
for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) <= m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds
r : ( ( ) ( V30() real ext-real ) Real) < seq : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V36() ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ;

attr seq is divergent_to-infty means :: LIMFUNC1:def 5
for r being ( ( ) ( V30() real ext-real ) Real) ex n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) st
for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) <= m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds
seq : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V36() ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V30() real ext-real ) Real) ;

end;

theorem :: LIMFUNC1:6

theorem :: LIMFUNC1:7

for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) )
for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) holds
( ( seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) subsequence of b₂ : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) is divergent_to+infty implies seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty ) & ( seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) subsequence of b₂ : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) is divergent_to-infty implies seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty ) ) ;

theorem :: LIMFUNC1:8

theorem :: LIMFUNC1:9

theorem :: LIMFUNC1:10

theorem :: LIMFUNC1:11

theorem :: LIMFUNC1:12

theorem :: LIMFUNC1:13

for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence)
for r being ( ( ) ( V30() real ext-real ) Real) holds
( ( seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ) & ( seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & r : ( ( ) ( V30() real ext-real ) Real) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ) & ( r : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies ( rng (r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) = {0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( V47() V48() V49() V50() V51() V52() ) set ) & r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant ) ) ) ;

theorem :: LIMFUNC1:14

for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence)
for r being ( ( ) ( V30() real ext-real ) Real) holds
( ( seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ) & ( seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & r : ( ( ) ( V30() real ext-real ) Real) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ) & ( r : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies ( rng (r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) = {0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( V47() V48() V49() V50() V51() V52() ) set ) & r : ( ( ) ( V30() real ext-real ) Real) (#) seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant ) ) ) ;

theorem :: LIMFUNC1:15

theorem :: LIMFUNC1:16

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is bounded_below & seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty holds
seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) - seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ;

theorem :: LIMFUNC1:17

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is bounded_above & seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty holds
seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) - seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ;

theorem :: LIMFUNC1:18

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent holds
seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) + seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ;

theorem :: LIMFUNC1:19

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent holds
seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) + seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ;

theorem :: LIMFUNC1:20

theorem :: LIMFUNC1:21

theorem :: LIMFUNC1:22

for seq1, seq2 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & ex r being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) >= r : ( ( ) ( V30() real ext-real ) Real) ) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) (#) seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ;

theorem :: LIMFUNC1:23

for seq1, seq2 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & ex r being ( ( ) ( V30() real ext-real ) Real) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V30() real ext-real ) Real) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) >= r : ( ( ) ( V30() real ext-real ) Real) ) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) (#) seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ;

theorem :: LIMFUNC1:24

theorem :: LIMFUNC1:25

theorem :: LIMFUNC1:26

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is ( ( ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) subsequence of seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty ;

theorem :: LIMFUNC1:27

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is ( ( ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) subsequence of seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty ;

theorem :: LIMFUNC1:28

for seq1, seq2 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < lim seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) (#) seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ;

theorem :: LIMFUNC1:29

theorem :: LIMFUNC1:30

theorem :: LIMFUNC1:31

theorem :: LIMFUNC1:32

theorem :: LIMFUNC1:33

theorem :: LIMFUNC1:34

theorem :: LIMFUNC1:35

theorem :: LIMFUNC1:36

theorem :: LIMFUNC1:37

theorem :: LIMFUNC1:38

theorem :: LIMFUNC1:39

theorem :: LIMFUNC1:40

theorem :: LIMFUNC1:41

for seq1, seq2 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is bounded & ( seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty or seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty ) holds
( seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) /" seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) /" seq2 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LIMFUNC1:42

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty ;

theorem :: LIMFUNC1:43

for seq, seq1 being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) holds
seq1 : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty ;

definition

attr f is convergent_in+infty means :: LIMFUNC1:def 6
( ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex g being ( ( ) ( V30() real ext-real ) Real) st
for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( ) ( V30() real ext-real ) Real) is divergent_to+infty & rng seq : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( ) ( V30() real ext-real ) Real) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( ) ( V30() real ext-real ) Real) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = g : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) );

attr f is divergent_in+infty_to+infty means :: LIMFUNC1:def 7
( ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & rng seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ) );

attr f is divergent_in+infty_to-infty means :: LIMFUNC1:def 8
( ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & rng seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ) );

attr f is convergent_in-infty means :: LIMFUNC1:def 9
( ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex g being ( ( ) ( V30() real ext-real ) Real) st
for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( ) ( V30() real ext-real ) Real) is divergent_to-infty & rng seq : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( ) ( V30() real ext-real ) Real) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( ) ( V30() real ext-real ) Real) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = g : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) );

attr f is divergent_in-infty_to+infty means :: LIMFUNC1:def 10
( ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & rng seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to+infty ) );

attr f is divergent_in-infty_to-infty means :: LIMFUNC1:def 11
( ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & rng seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_to-infty ) );

end;

theorem :: LIMFUNC1:44

theorem :: LIMFUNC1:45

theorem :: LIMFUNC1:46

theorem :: LIMFUNC1:47

theorem :: LIMFUNC1:48

theorem :: LIMFUNC1:49

theorem :: LIMFUNC1:50

theorem :: LIMFUNC1:51

theorem :: LIMFUNC1:52

theorem :: LIMFUNC1:53

theorem :: LIMFUNC1:54

theorem :: LIMFUNC1:55

theorem :: LIMFUNC1:56

theorem :: LIMFUNC1:57

theorem :: LIMFUNC1:58

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,)
for r being ( ( ) ( V30() real ext-real ) Real) holds
( ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to+infty & r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in+infty_to+infty ) & ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to+infty & r : ( ( ) ( V30() real ext-real ) Real) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in+infty_to-infty ) & ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to-infty & r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in+infty_to-infty ) & ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to-infty & r : ( ( ) ( V30() real ext-real ) Real) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in+infty_to+infty ) ) ;

theorem :: LIMFUNC1:59

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,)
for r being ( ( ) ( V30() real ext-real ) Real) holds
( ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to+infty & r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in-infty_to+infty ) & ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to+infty & r : ( ( ) ( V30() real ext-real ) Real) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in-infty_to-infty ) & ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to-infty & r : ( ( ) ( V30() real ext-real ) Real) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in-infty_to-infty ) & ( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to-infty & r : ( ( ) ( V30() real ext-real ) Real) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) implies r : ( ( ) ( V30() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in-infty_to+infty ) ) ;

theorem :: LIMFUNC1:60

theorem :: LIMFUNC1:61

theorem :: LIMFUNC1:62

theorem :: LIMFUNC1:63

theorem :: LIMFUNC1:64

theorem :: LIMFUNC1:65

theorem :: LIMFUNC1:66

theorem :: LIMFUNC1:67

theorem :: LIMFUNC1:68

theorem :: LIMFUNC1:69

theorem :: LIMFUNC1:70

for f1, f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to+infty & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to+infty ;

theorem :: LIMFUNC1:71

for f1, f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to-infty & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in+infty_to-infty ;

theorem :: LIMFUNC1:72

for f1, f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to+infty & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to+infty ;

theorem :: LIMFUNC1:73

for f1, f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to-infty & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is divergent_in-infty_to-infty ;

theorem :: LIMFUNC1:74

theorem :: LIMFUNC1:75

theorem :: LIMFUNC1:76

theorem :: LIMFUNC1:77

definition

let f be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
assume f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty ;

func lim_in+infty f -> ( ( ) ( V30() real ext-real ) Real) means :: LIMFUNC1:def 12
for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to+infty & rng seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = it : ( ( ) ( ) set ) );

end;

definition

func lim_in-infty f -> ( ( ) ( V30() real ext-real ) Real) means :: LIMFUNC1:def 13
for seq being ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is divergent_to-infty & rng seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (f : ( ( V1() V6() natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V47() V48() V49() V50() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued natural-valued ) set ) /* seq : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = it : ( ( ) ( ) set ) );

end;

theorem :: LIMFUNC1:78

theorem :: LIMFUNC1:79

theorem :: LIMFUNC1:80

theorem :: LIMFUNC1:81

theorem :: LIMFUNC1:82

theorem :: LIMFUNC1:83

theorem :: LIMFUNC1:84

theorem :: LIMFUNC1:85

theorem :: LIMFUNC1:86

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent_in+infty & lim_in+infty (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Real) = (lim_in+infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V30() real ext-real ) Real) " : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ;

theorem :: LIMFUNC1:87

theorem :: LIMFUNC1:88

for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent_in+infty & lim_in+infty (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Real) = (lim_in+infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V30() real ext-real ) Real) / (lim_in+infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ;

theorem :: LIMFUNC1:89

theorem :: LIMFUNC1:90

theorem :: LIMFUNC1:91

theorem :: LIMFUNC1:92

theorem :: LIMFUNC1:93

theorem :: LIMFUNC1:94

theorem :: LIMFUNC1:95

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent_in-infty & lim_in-infty (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Real) = (lim_in-infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V30() real ext-real ) Real) " : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ;

theorem :: LIMFUNC1:96

theorem :: LIMFUNC1:97

for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent_in-infty & lim_in-infty (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Real) = (lim_in-infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V30() real ext-real ) Real) / (lim_in-infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ;

theorem :: LIMFUNC1:98

for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent_in+infty & lim_in+infty (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LIMFUNC1:99

for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent_in-infty & lim_in-infty (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LIMFUNC1:100

for f1, f2, f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = lim_in+infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( ( ( (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) or ( (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = lim_in+infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) ) ;

theorem :: LIMFUNC1:101

theorem :: LIMFUNC1:102

for f1, f2, f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = lim_in-infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
( ( ( (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) or ( (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = lim_in-infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) ) ;

theorem :: LIMFUNC1:103

theorem :: LIMFUNC1:104

for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & ex r being ( ( ) ( V30() real ext-real ) Real) st
( ( (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) or ( (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) ) holds
lim_in+infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) <= lim_in+infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) ;

theorem :: LIMFUNC1:105

for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & ex r being ( ( ) ( V30() real ext-real ) Real) st
( ( (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) or ( (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) c= (dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ) ) holds
lim_in-infty f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) <= lim_in-infty f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) ;

theorem :: LIMFUNC1:106

theorem :: LIMFUNC1:107

theorem :: LIMFUNC1:108

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) <= f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in+infty_to+infty ;

theorem :: LIMFUNC1:109

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in+infty & lim_in+infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( r : ( ( ) ( V30() real ext-real ) Real) < g : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (right_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in+infty_to-infty ;

theorem :: LIMFUNC1:110

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) <= f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in-infty_to+infty ;

theorem :: LIMFUNC1:111

for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is convergent_in-infty & lim_in-infty f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V30() real ext-real ) Real) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V30() real ext-real ) Real) ex g being ( ( ) ( V30() real ext-real ) Real) st
( g : ( ( ) ( V30() real ext-real ) Real) < r : ( ( ) ( V30() real ext-real ) Real) & g : ( ( ) ( V30() real ext-real ) Real) in dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & ex r being ( ( ) ( V30() real ext-real ) Real) st
for g being ( ( ) ( V30() real ext-real ) Real) st g : ( ( ) ( V30() real ext-real ) Real) in (dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) /\ (left_open_halfline r : ( ( ) ( V30() real ext-real ) Real) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V30() real ext-real ) Real) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is divergent_in-infty_to-infty ;

theorem :: LIMFUNC1:112

theorem :: LIMFUNC1:113

theorem :: LIMFUNC1:114

theorem :: LIMFUNC1:115