PREPOWER

:: PREPOWER semantic presentation

begin

registration

let i be ( ( integer ) ( V30() real ext-real integer rational ) Integer) ;

cluster |.i : ( ( integer ) ( V30() real ext-real integer rational ) set ) .| : ( ( real ) ( V30() real ext-real rational ) set ) -> natural real ;

end;

theorem :: PREPOWER:1

theorem :: PREPOWER:2

definition

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

func a GeoSeq -> ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) means :: PREPOWER:def 1
for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( V11() ) ( V11() ) set ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( ) ( ) set ) |^ m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ;

end;

theorem :: PREPOWER:3

for a being ( ( real ) ( V30() real ext-real ) number )
for s1 being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) holds
( s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) = a : ( ( real ) ( V30() real ext-real ) number ) GeoSeq : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) iff ( s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . (m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = (s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) * a : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ) ) ;

theorem :: PREPOWER:4

for a being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) <> 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds (a : ( ( real ) ( V30() real ext-real ) number ) GeoSeq) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) <> 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:5

theorem :: PREPOWER:6

theorem :: PREPOWER:7

theorem :: PREPOWER:8

for b, a being ( ( real ) ( V30() real ext-real ) number )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) holds (b : ( ( real ) ( V30() real ext-real ) number ) / a : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) : ( ( ) ( V30() real ext-real ) set ) = (b : ( ( real ) ( V30() real ext-real ) number ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) ) : ( ( ) ( V30() real ext-real ) set ) / (a : ( ( real ) ( V30() real ext-real ) number ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) ;

theorem :: PREPOWER:9

for a, b being ( ( real ) ( V30() real ext-real ) number )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) st 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) < a : ( ( real ) ( V30() real ext-real ) number ) & a : ( ( real ) ( V30() real ext-real ) number ) <= b : ( ( real ) ( V30() real ext-real ) number ) holds
a : ( ( real ) ( V30() real ext-real ) number ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) : ( ( ) ( V30() real ext-real ) set ) <= b : ( ( real ) ( V30() real ext-real ) number ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:10

theorem :: PREPOWER:11

theorem :: PREPOWER:12

theorem :: PREPOWER:13

theorem :: PREPOWER:14

theorem :: PREPOWER:15

theorem :: PREPOWER:16

theorem :: PREPOWER:17

theorem :: PREPOWER:18

for m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) )
for s1, s2 being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = (s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) |^ m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) holds
( s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = (lim s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) |^ m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ;

definition

let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) ;
let a be ( ( real ) ( V30() real ext-real ) number ) ;
assume 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) <= n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) ;

func n -Root a -> ( ( real ) ( V30() real ext-real ) number ) means :: PREPOWER:def 2
( it : ( ( ) ( V30() ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) |^ n : ( ( ) ( ) set ) : ( ( ) ( ) set ) = a : ( ( V11() ) ( V11() ) set ) & it : ( ( ) ( V30() ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) if a : ( ( V11() ) ( V11() ) set ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) )
it : ( ( ) ( V30() ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) = 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) if a : ( ( V11() ) ( V11() ) set ) = 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) )
;

end;

definition

let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;
let a be ( ( ) ( V30() real ext-real ) Real) ;
:: original: -Root
redefine func n -Root a -> ( ( ) ( V30() real ext-real ) Real) ;

end;

theorem :: PREPOWER:19

theorem :: PREPOWER:20

theorem :: PREPOWER:21

for a being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) -Root a : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) = a : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:22

theorem :: PREPOWER:23

theorem :: PREPOWER:24

theorem :: PREPOWER:25

theorem :: PREPOWER:26

theorem :: PREPOWER:27

theorem :: PREPOWER:28

theorem :: PREPOWER:29

theorem :: PREPOWER:30

theorem :: PREPOWER:31

theorem :: PREPOWER:32

for a being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
2 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) -Root a : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) = sqrt a : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:33

for a being ( ( real ) ( V30() real ext-real ) number )
for s being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
s : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) -Root a : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) ) holds
( s : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

definition

let a be ( ( real ) ( V30() real ext-real ) number ) ;
let k be ( ( integer ) ( V30() real ext-real integer rational ) Integer) ;

func a #Z k -> ( ( ) ( ) set ) equals :: PREPOWER:def 3
a : ( ( ) ( ) set ) |^ (abs k : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) if k : ( ( V11() ) ( V11() ) set ) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) )
(a : ( ( ) ( ) set ) |^ (abs k : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) " : ( ( V30() ) ( V30() ) set ) if k : ( ( V11() ) ( V11() ) set ) < 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) )
;

end;

registration

let a be ( ( real ) ( V30() real ext-real ) number ) ;
let k be ( ( integer ) ( V30() real ext-real integer rational ) Integer) ;

cluster a : ( ( real ) ( V30() real ext-real ) set ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) set ) : ( ( ) ( ) set ) -> real ;

end;

definition

let a be ( ( ) ( V30() real ext-real ) Real) ;
let k be ( ( integer ) ( V30() real ext-real integer rational ) Integer) ;
:: original: #Z
redefine func a #Z k -> ( ( ) ( V30() real ext-real ) Real) ;

end;

theorem :: PREPOWER:34

for a being ( ( real ) ( V30() real ext-real ) number ) holds a : ( ( real ) ( V30() real ext-real ) number ) #Z 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) set ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:35

for a being ( ( real ) ( V30() real ext-real ) number ) holds a : ( ( real ) ( V30() real ext-real ) number ) #Z 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) set ) = a : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:36

for a being ( ( real ) ( V30() real ext-real ) number )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) holds a : ( ( real ) ( V30() real ext-real ) number ) #Z n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) : ( ( ) ( V30() real ext-real ) set ) = a : ( ( real ) ( V30() real ext-real ) number ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational ) Nat) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:37

for k being ( ( integer ) ( V30() real ext-real integer rational ) Integer) holds 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) Real) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:38

for a being ( ( real ) ( V30() real ext-real ) number )
for k being ( ( integer ) ( V30() real ext-real integer rational ) Integer) st a : ( ( real ) ( V30() real ext-real ) number ) <> 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) <> 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:39

for a being ( ( real ) ( V30() real ext-real ) number )
for k being ( ( integer ) ( V30() real ext-real integer rational ) Integer) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:40

for a, b being ( ( real ) ( V30() real ext-real ) number )
for k being ( ( integer ) ( V30() real ext-real integer rational ) Integer) holds (a : ( ( real ) ( V30() real ext-real ) number ) * b : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) = (a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) * (b : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:41

for a being ( ( real ) ( V30() real ext-real ) number )
for k being ( ( integer ) ( V30() real ext-real integer rational ) Integer) holds a : ( ( real ) ( V30() real ext-real ) number ) #Z (- k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( V30() ) ( V30() real ext-real integer rational ) set ) : ( ( ) ( V30() real ext-real ) set ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ;

theorem :: PREPOWER:42

for a being ( ( real ) ( V30() real ext-real ) number )
for k being ( ( integer ) ( V30() real ext-real integer rational ) Integer) holds (1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) Real) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ;

theorem :: PREPOWER:43

theorem :: PREPOWER:44

for a being ( ( real ) ( V30() real ext-real ) number )
for k, l being ( ( integer ) ( V30() real ext-real integer rational ) Integer) st a : ( ( real ) ( V30() real ext-real ) number ) <> 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Z (k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) + l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real integer rational ) set ) : ( ( ) ( V30() real ext-real ) set ) = (a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) * (a : ( ( real ) ( V30() real ext-real ) number ) #Z l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:45

for a being ( ( real ) ( V30() real ext-real ) number )
for k, l being ( ( integer ) ( V30() real ext-real integer rational ) Integer) holds (a : ( ( real ) ( V30() real ext-real ) number ) #Z k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real ) set ) #Z l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) = a : ( ( real ) ( V30() real ext-real ) number ) #Z (k : ( ( integer ) ( V30() real ext-real integer rational ) Integer) * l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) ) : ( ( ) ( V30() real ext-real integer rational ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:46

definition

let a be ( ( real ) ( V30() real ext-real ) number ) ;
let p be ( ( rational ) ( V30() real ext-real rational ) Rational) ;

func a #Q p -> ( ( ) ( ) set ) equals :: PREPOWER:def 4
(denominator p : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) -Root (a : ( ( ) ( ) set ) #Z (numerator p : ( ( V11() ) ( V11() ) set ) ) : ( ( integer ) ( V30() real ext-real integer rational ) set ) ) : ( ( ) ( ) set ) : ( ( real ) ( V30() real ext-real ) number ) ;

end;

registration

let a be ( ( real ) ( V30() real ext-real ) number ) ;
let p be ( ( rational ) ( V30() real ext-real rational ) Rational) ;

cluster a : ( ( real ) ( V30() real ext-real ) set ) #Q p : ( ( rational ) ( V30() real ext-real rational ) set ) : ( ( ) ( ) set ) -> real ;

end;

definition

let a be ( ( ) ( V30() real ext-real ) Real) ;
let p be ( ( rational ) ( V30() real ext-real rational ) Rational) ;
:: original: #Q
redefine func a #Q p -> ( ( ) ( V30() real ext-real ) Real) ;

end;

theorem :: PREPOWER:47

theorem :: PREPOWER:48

theorem :: PREPOWER:49

theorem :: PREPOWER:50

theorem :: PREPOWER:51

for p being ( ( rational ) ( V30() real ext-real rational ) Rational) holds 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) Real) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:52

theorem :: PREPOWER:53

for a being ( ( real ) ( V30() real ext-real ) number )
for p, q being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) * (a : ( ( real ) ( V30() real ext-real ) number ) #Q q : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) set ) = a : ( ( real ) ( V30() real ext-real ) number ) #Q (p : ( ( rational ) ( V30() real ext-real rational ) Rational) + q : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real rational ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:54

for a being ( ( real ) ( V30() real ext-real ) number )
for p being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( real ) ( V30() real ext-real ) number ) #Q (- p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( V30() ) ( V30() real ext-real rational ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:55

for a being ( ( real ) ( V30() real ext-real ) number )
for p, q being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) / (a : ( ( real ) ( V30() real ext-real ) number ) #Q q : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) = a : ( ( real ) ( V30() real ext-real ) number ) #Q (p : ( ( rational ) ( V30() real ext-real rational ) Rational) - q : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real rational ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:56

for a, b being ( ( real ) ( V30() real ext-real ) number )
for p being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) * b : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) = (a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) * (b : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:57

for a being ( ( real ) ( V30() real ext-real ) number )
for p being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) Real) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ;

theorem :: PREPOWER:58

for a, b being ( ( real ) ( V30() real ext-real ) number )
for p being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) / b : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) = (a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) / (b : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) ;

theorem :: PREPOWER:59

for a being ( ( real ) ( V30() real ext-real ) number )
for p, q being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real ) set ) #Q q : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) = a : ( ( real ) ( V30() real ext-real ) number ) #Q (p : ( ( rational ) ( V30() real ext-real rational ) Rational) * q : ( ( rational ) ( V30() real ext-real rational ) Rational) ) : ( ( ) ( V30() real ext-real rational ) set ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:60

for a being ( ( real ) ( V30() real ext-real ) number )
for p being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( rational ) ( V30() real ext-real rational ) Rational) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:61

for a being ( ( real ) ( V30() real ext-real ) number )
for p being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( rational ) ( V30() real ext-real rational ) Rational) <= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) <= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:62

theorem :: PREPOWER:63

for a being ( ( real ) ( V30() real ext-real ) number )
for p, q being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( rational ) ( V30() real ext-real rational ) Rational) >= q : ( ( rational ) ( V30() real ext-real rational ) Rational) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) >= a : ( ( real ) ( V30() real ext-real ) number ) #Q q : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:64

for a being ( ( real ) ( V30() real ext-real ) number )
for p, q being ( ( rational ) ( V30() real ext-real rational ) Rational) st a : ( ( real ) ( V30() real ext-real ) number ) > 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( rational ) ( V30() real ext-real rational ) Rational) > q : ( ( rational ) ( V30() real ext-real rational ) Rational) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) > a : ( ( real ) ( V30() real ext-real ) number ) #Q q : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:65

theorem :: PREPOWER:66

registration

cluster Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued for ( ( ) ( ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ;

end;

definition

canceled;
mode Rational_Sequence is ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ;

end;

theorem :: PREPOWER:67

for a being ( ( real ) ( V30() real ext-real ) number ) ex s being ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) st
( s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) is convergent & lim s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( real ) ( V30() real ext-real ) number ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real rational ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) <= a : ( ( real ) ( V30() real ext-real ) number ) ) ) ;

theorem :: PREPOWER:68

for a being ( ( real ) ( V30() real ext-real ) number ) ex s being ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) st
( s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) is convergent & lim s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( real ) ( V30() real ext-real ) number ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real rational ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) >= a : ( ( real ) ( V30() real ext-real ) number ) ) ) ;

definition

let a be ( ( real ) ( V30() real ext-real ) number ) ;
let s be ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) ;

func a #Q s -> ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) means :: PREPOWER:def 6
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( V30() ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( ) ( ) set ) #Q (s : ( ( V11() ) ( V11() ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ;

end;

theorem :: PREPOWER:69

for a being ( ( real ) ( V30() real ext-real ) number )
for s being ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) st s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) is convergent & a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Q s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent ;

theorem :: PREPOWER:70

for s1, s2 being ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence)
for a being ( ( real ) ( V30() real ext-real ) number ) st s1 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) is convergent & s2 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) is convergent & lim s1 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = lim s2 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) & a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( a : ( ( real ) ( V30() real ext-real ) number ) #Q s1 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & a : ( ( real ) ( V30() real ext-real ) number ) #Q s2 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim (a : ( ( real ) ( V30() real ext-real ) number ) #Q s1 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = lim (a : ( ( real ) ( V30() real ext-real ) number ) #Q s2 : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ;

definition

let a, b be ( ( real ) ( V30() real ext-real ) number ) ;
assume a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

func a #R b -> ( ( real ) ( V30() real ext-real ) number ) means :: PREPOWER:def 7
ex s being ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) st
( s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) is convergent & lim s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = b : ( ( V11() ) ( V11() ) set ) & a : ( ( ) ( ) set ) #Q s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim (a : ( ( ) ( ) set ) #Q s : ( ( RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued RAT : ( ( ) ( V11() V51() V52() V53() V54() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Rational_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = it : ( ( ) ( V30() ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) );

end;

definition

let a, b be ( ( ) ( V30() real ext-real ) Real) ;
:: original: #R
redefine func a #R b -> ( ( ) ( V30() real ext-real ) Real) ;

end;

theorem :: PREPOWER:71

for a being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V30() real ext-real ) number ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:72

for a being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V30() real ext-real ) number ) = a : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:73

for a being ( ( real ) ( V30() real ext-real ) number ) holds 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) #R a : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:74

theorem :: PREPOWER:75

theorem :: PREPOWER:76

for a, c being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R (- c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( V30() ) ( V30() real ext-real ) set ) : ( ( real ) ( V30() real ext-real ) number ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ;

theorem :: PREPOWER:77

theorem :: PREPOWER:78

for a, b, c being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) * b : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) set ) #R c : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) = (a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( real ) ( V30() real ext-real ) number ) * (b : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:79

for a, c being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) #R c : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ;

theorem :: PREPOWER:80

for a, b, c being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V30() real ext-real ) number ) / b : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) #R c : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) = (a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( real ) ( V30() real ext-real ) number ) / (b : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of COMPLEX : ( ( ) ( V11() V51() V57() V58() ) set ) ) ;

theorem :: PREPOWER:81

for a, b being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R b : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:82

for a, c, b being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V30() real ext-real ) number ) >= b : ( ( real ) ( V30() real ext-real ) number ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) >= a : ( ( real ) ( V30() real ext-real ) number ) #R b : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:83

for a, c, b being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V30() real ext-real ) number ) > b : ( ( real ) ( V30() real ext-real ) number ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) > a : ( ( real ) ( V30() real ext-real ) number ) #R b : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:84

for a, c, b being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V30() real ext-real ) number ) <= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V30() real ext-real ) number ) >= b : ( ( real ) ( V30() real ext-real ) number ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R c : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) <= a : ( ( real ) ( V30() real ext-real ) number ) #R b : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:85

for a, b being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V30() real ext-real ) number ) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R b : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:86

theorem :: PREPOWER:87

for a, b being ( ( real ) ( V30() real ext-real ) number ) st a : ( ( real ) ( V30() real ext-real ) number ) >= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V30() real ext-real ) number ) <= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #R b : ( ( real ) ( V30() real ext-real ) number ) : ( ( real ) ( V30() real ext-real ) number ) <= 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:88

theorem :: PREPOWER:89

for p being ( ( rational ) ( V30() real ext-real rational ) Rational)
for s1, s2 being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = (s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) Real) ) ) holds
lim s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = (lim s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) #Q p : ( ( rational ) ( V30() real ext-real rational ) Rational) : ( ( ) ( V30() real ext-real ) Real) ;

theorem :: PREPOWER:90

for a being ( ( real ) ( V30() real ext-real ) number )
for s1, s2 being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) & s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( real ) ( V30() real ext-real ) number ) #R (s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( real ) ( V30() real ext-real ) number ) ) holds
lim s2 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) = a : ( ( real ) ( V30() real ext-real ) number ) #R (lim s1 : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: PREPOWER:91

begin

theorem :: PREPOWER:92

theorem :: PREPOWER:93

theorem :: PREPOWER:94

theorem :: PREPOWER:95

theorem :: PREPOWER:96

theorem :: PREPOWER:97

theorem :: PREPOWER:98

for a being ( ( real ) ( V30() real ext-real ) number )
for l being ( ( integer ) ( V30() real ext-real integer rational ) Integer) st a : ( ( real ) ( V30() real ext-real ) number ) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Z l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) >= 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: PREPOWER:99

for a being ( ( real ) ( V30() real ext-real ) number )
for l being ( ( integer ) ( V30() real ext-real integer rational ) Integer) st a : ( ( real ) ( V30() real ext-real ) number ) > 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() ) Element of K19(REAL : ( ( ) ( V11() V51() V52() V53() V57() V58() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V30() real ext-real ) number ) #Q l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) = a : ( ( real ) ( V30() real ext-real ) number ) #Z l : ( ( integer ) ( V30() real ext-real integer rational ) Integer) : ( ( ) ( V30() real ext-real ) set ) ;

theorem :: PREPOWER:100