:: ASYMPT_0 semantic presentation

scheme :: ASYMPT_0:sch 1
s1{ F₁() -> Nat, F₂() -> Nat, F₃() -> non empty set , F₄( set ) -> Element of F₃() } :

{ F₄(b₁) where B is Nat : ( F₁() <= b₁ & b₁ <= F₂() ) } is non empty finite Subset of F₃()

provided

E1: F₁() <= F₂()

proof end;

scheme :: ASYMPT_0:sch 2
s2{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

{ F₃(b₁) where B is Nat : b₁ <= F₁() } is non empty finite Subset of F₂()

proof end;

scheme :: ASYMPT_0:sch 3
s3{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

{ F₃(b₁) where B is Nat : b₁ < F₁() } is non empty finite Subset of F₂()

provided

E1: F₁() > 0

proof end;

definition

let c₁ be real number ;
canceled;
canceled;
attr a₁ is logbase means :Def3: :: ASYMPT_0:def 3
( a₁ > 0 & a₁ <> 1 );

end;

:: deftheorem Def1 ASYMPT_0:def 1 :

:: deftheorem Def2 ASYMPT_0:def 2 :

:: deftheorem Def3 defines logbase ASYMPT_0:def 3 :

registration

cluster positive Element of REAL ;
existence

proof end;

cluster negative Element of REAL ;
existence

proof end;

cluster logbase Element of REAL ;
existence

proof end;

cluster non negative Element of REAL ;
existence by XREAL_0:def 4;
cluster non positive Element of REAL ;
existence by XREAL_0:def 3;
cluster non logbase Element of REAL ;
existence

proof end;

end;

definition

let c₁ be Real_Sequence;
attr a₁ is eventually-nonnegative means :Def4: :: ASYMPT_0:def 4
ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
a₁ . b₂ >= 0;
attr a₁ is positive means :Def5: :: ASYMPT_0:def 5
for b₁ being Nat holds a₁ . b₁ > 0;
attr a₁ is eventually-positive means :Def6: :: ASYMPT_0:def 6
ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
a₁ . b₂ > 0;
attr a₁ is eventually-nonzero means :Def7: :: ASYMPT_0:def 7
ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
a₁ . b₂ <> 0;
attr a₁ is eventually-nondecreasing means :Def8: :: ASYMPT_0:def 8
ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
a₁ . b₂ <= a₁ . (b₂ + 1);

end;

:: deftheorem Def4 defines eventually-nonnegative ASYMPT_0:def 4 :

:: deftheorem Def5 defines positive ASYMPT_0:def 5 :

:: deftheorem Def6 defines eventually-positive ASYMPT_0:def 6 :

:: deftheorem Def7 defines eventually-nonzero ASYMPT_0:def 7 :

:: deftheorem Def8 defines eventually-nondecreasing ASYMPT_0:def 8 :

registration

cluster eventually-nonnegative positive eventually-positive eventually-nonzero eventually-nondecreasing M5( NAT , REAL );
existence

proof end;

end;

registration

cluster positive -> eventually-positive M5( NAT , REAL );
coherence

proof end;

cluster eventually-positive -> eventually-nonnegative eventually-nonzero M5( NAT , REAL );
coherence

proof end;

cluster eventually-nonnegative eventually-nonzero -> eventually-positive M5( NAT , REAL );
coherence

proof end;

end;

definition

let c₁, c₂ be eventually-nonnegative Real_Sequence;
redefine func + as c₁ + c₂ -> eventually-nonnegative Real_Sequence;
coherence

proof end;

end;

definition

let c₁ be Real_Sequence;
let c₂ be real number ;
func c₂ + c₁ -> Real_Sequence means :Def9: :: ASYMPT_0:def 9
for b₁ being Nat holds a₃ . b₁ = a₂ + (a₁ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines + ASYMPT_0:def 9 :

notation

let c₁ be Real_Sequence;
let c₂ be real number ;
synonym c₁ + c₂ for c₂ + c₁;

end;

definition

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be positive Real;
redefine func (#) as c₂ (#) c₁ -> eventually-nonnegative Real_Sequence;
coherence

proof end;

end;

registration

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be non negative Real;
cluster a₂ + a₁ -> eventually-nonnegative ;
coherence

proof end;

end;

registration

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be positive Real;
cluster a₂ + a₁ -> eventually-nonnegative eventually-positive eventually-nonzero ;
coherence

proof end;

end;

definition

let c₁, c₂ be Real_Sequence;
func max c₁,c₂ -> Real_Sequence means :Def10: :: ASYMPT_0:def 10
for b₁ being Nat holds a₃ . b₁ = max (a₁ . b₁),(a₂ . b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def10 defines max ASYMPT_0:def 10 :

registration

let c₁ be Real_Sequence;
let c₂ be eventually-nonnegative Real_Sequence;
cluster max a₁,a₂ -> eventually-nonnegative ;
coherence

proof end;

end;

registration

let c₁ be Real_Sequence;
let c₂ be eventually-positive Real_Sequence;
cluster max a₁,a₂ -> eventually-nonnegative eventually-positive eventually-nonzero ;
coherence

proof end;

end;

definition

let c₁, c₂ be Real_Sequence;
pred c₂ majorizes c₁ means :Def11: :: ASYMPT_0:def 11
ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
a₁ . b₂ <= a₂ . b₂;

end;

:: deftheorem Def11 defines majorizes ASYMPT_0:def 11 :

Lemma10: for b₁, b₂ being Real_Sequence
for b₃ being Nat holds (b₁ /" b₂) . b₃ = (b₁ . b₃) / (b₂ . b₃)

proof end;

theorem Th1: :: ASYMPT_0:1

for b₁ being Real_Sequence
for b₂ being Nat st ( for b₃ being Nat st b₃ >= b₂ holds
b₁ . b₃ <= b₁ . (b₃ + 1) ) holds
for b₃, b₄ being Nat st b₂ <= b₃ & b₃ <= b₄ holds
b₁ . b₃ <= b₁ . b₄

proof end;

theorem Th2: :: ASYMPT_0:2

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) <> 0 holds
( b₂ /" b₁ is convergent & lim (b₂ /" b₁) = (lim (b₁ /" b₂)) " )

proof end;

theorem Th3: :: ASYMPT_0:3

for b₁ being eventually-nonnegative Real_Sequence st b₁ is convergent holds
0 <= lim b₁

proof end;

theorem Th4: :: ASYMPT_0:4

for b₁, b₂ being Real_Sequence st b₁ is convergent & b₂ is convergent & b₂ majorizes b₁ holds
lim b₁ <= lim b₂

proof end;

theorem Th5: :: ASYMPT_0:5

for b₁ being Real_Sequence
for b₂ being eventually-nonzero Real_Sequence st b₁ /" b₂ is divergent_to+infty holds
( b₂ /" b₁ is convergent & lim (b₂ /" b₁) = 0 )

proof end;

definition

let c₁ be eventually-nonnegative Real_Sequence;
func Big_Oh c₁ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 12
{ b₁ where B is Element of Funcs NAT ,REAL : ex b₁ being Realex b₂ being Nat st
( b₂ > 0 & ( for b₃ being Nat st b₄ >= b₃ holds
( b₁ . b₄ <= b₂ * (a₁ . b₄) & b₁ . b₄ >= 0 ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def12 defines Big_Oh ASYMPT_0:def 12 :

theorem Th6: :: ASYMPT_0:6

for b₁ being set
for b₂ being eventually-nonnegative Real_Sequence st b₁ in Big_Oh b₂ holds
b₁ is eventually-nonnegative Real_Sequence

proof end;

theorem Th7: :: ASYMPT_0:7

for b₁ being positive Real_Sequence
for b₂ being eventually-nonnegative Real_Sequence holds
( b₂ in Big_Oh b₁ iff ex b₃ being Real st
( b₃ > 0 & ( for b₄ being Nat holds b₂ . b₄ <= b₃ * (b₁ . b₄) ) ) )

proof end;

theorem Th8: :: ASYMPT_0:8

for b₁ being eventually-positive Real_Sequence
for b₂ being eventually-nonnegative Real_Sequence
for b₃ being Nat st b₂ in Big_Oh b₁ & ( for b₄ being Nat st b₄ >= b₃ holds
b₁ . b₄ > 0 ) holds
ex b₄ being Real st
( b₄ > 0 & ( for b₅ being Nat st b₅ >= b₃ holds
b₂ . b₅ <= b₄ * (b₁ . b₅) ) )

proof end;

theorem Th9: :: ASYMPT_0:9

for b₁, b₂ being eventually-nonnegative Real_Sequence holds Big_Oh (b₁ + b₂) = Big_Oh (max b₁,b₂)

proof end;

theorem Th10: :: ASYMPT_0:10

for b₁ being eventually-nonnegative Real_Sequence holds b₁ in Big_Oh b₁

proof end;

theorem Th11: :: ASYMPT_0:11

for b₁, b₂ being eventually-nonnegative Real_Sequence st b₁ in Big_Oh b₂ holds
Big_Oh b₁ c= Big_Oh b₂

proof end;

theorem Th12: :: ASYMPT_0:12

for b₁, b₂, b₃ being eventually-nonnegative Real_Sequence st b₁ in Big_Oh b₂ & b₂ in Big_Oh b₃ holds
b₁ in Big_Oh b₃

proof end;

Lemma20: for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( ( b₁ in Big_Oh b₂ & b₂ in Big_Oh b₁ ) iff Big_Oh b₁ = Big_Oh b₂ )

proof end;

theorem Th13: :: ASYMPT_0:13

for b₁ being eventually-nonnegative Real_Sequence
for b₂ being positive Real holds Big_Oh b₁ = Big_Oh (b₂ (#) b₁)

proof end;

theorem Th14: :: ASYMPT_0:14

for b₁ being non negative Real
for b₂, b₃ being eventually-nonnegative Real_Sequence st b₂ in Big_Oh b₃ holds
b₂ in Big_Oh (b₁ + b₃)

proof end;

Lemma21: for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) > 0 holds
b₁ in Big_Oh b₂

proof end;

theorem Th15: :: ASYMPT_0:15

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) > 0 holds
Big_Oh b₁ = Big_Oh b₂

proof end;

theorem Th16: :: ASYMPT_0:16

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) = 0 holds
( b₁ in Big_Oh b₂ & not b₂ in Big_Oh b₁ )

proof end;

theorem Th17: :: ASYMPT_0:17

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is divergent_to+infty holds
( not b₁ in Big_Oh b₂ & b₂ in Big_Oh b₁ )

proof end;

definition

let c₁ be eventually-nonnegative Real_Sequence;
func Big_Omega c₁ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 13
{ b₁ where B is Element of Funcs NAT ,REAL : ex b₁ being Realex b₂ being Nat st
( b₂ > 0 & ( for b₃ being Nat st b₄ >= b₃ holds
( b₁ . b₄ >= b₂ * (a₁ . b₄) & b₁ . b₄ >= 0 ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def13 defines Big_Omega ASYMPT_0:def 13 :

theorem Th18: :: ASYMPT_0:18

for b₁ being set
for b₂ being eventually-nonnegative Real_Sequence st b₁ in Big_Omega b₂ holds
b₁ is eventually-nonnegative Real_Sequence

proof end;

theorem Th19: :: ASYMPT_0:19

for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( b₁ in Big_Omega b₂ iff b₂ in Big_Oh b₁ )

proof end;

theorem Th20: :: ASYMPT_0:20

for b₁ being eventually-nonnegative Real_Sequence holds b₁ in Big_Omega b₁

proof end;

theorem Th21: :: ASYMPT_0:21

for b₁, b₂, b₃ being eventually-nonnegative Real_Sequence st b₁ in Big_Omega b₂ & b₂ in Big_Omega b₃ holds
b₁ in Big_Omega b₃

proof end;

theorem Th22: :: ASYMPT_0:22

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) > 0 holds
Big_Omega b₁ = Big_Omega b₂

proof end;

theorem Th23: :: ASYMPT_0:23

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) = 0 holds
( b₂ in Big_Omega b₁ & not b₁ in Big_Omega b₂ )

proof end;

theorem Th24: :: ASYMPT_0:24

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is divergent_to+infty holds
( not b₂ in Big_Omega b₁ & b₁ in Big_Omega b₂ )

proof end;

theorem Th25: :: ASYMPT_0:25

for b₁, b₂ being positive Real_Sequence holds
( b₂ in Big_Omega b₁ iff ex b₃ being Real st
( b₃ > 0 & ( for b₄ being Nat holds b₃ * (b₁ . b₄) <= b₂ . b₄ ) ) )

proof end;

theorem Th26: :: ASYMPT_0:26

for b₁, b₂ being eventually-nonnegative Real_Sequence holds Big_Omega (b₁ + b₂) = Big_Omega (max b₁,b₂)

proof end;

definition

let c₁ be eventually-nonnegative Real_Sequence;
func Big_Theta c₁ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 14
(Big_Oh a₁) /\ (Big_Omega a₁);
coherence

proof end;

end;

:: deftheorem Def14 defines Big_Theta ASYMPT_0:def 14 :

theorem Th27: :: ASYMPT_0:27

for b₁ being eventually-nonnegative Real_Sequence holds Big_Theta b₁ = { b₂ where B is Element of Funcs NAT ,REAL : ex b₁, b₂ being Realex b₃ being Nat st
( b₃ > 0 & b₄ > 0 & ( for b₄ being Nat st b₆ >= b₅ holds
( b₄ * (b₁ . b₆) <= b₂ . b₆ & b₂ . b₆ <= b₃ * (b₁ . b₆) ) ) ) }

proof end;

theorem Th28: :: ASYMPT_0:28

for b₁ being eventually-nonnegative Real_Sequence holds b₁ in Big_Theta b₁

proof end;

theorem Th29: :: ASYMPT_0:29

for b₁, b₂ being eventually-nonnegative Real_Sequence st b₁ in Big_Theta b₂ holds
b₂ in Big_Theta b₁

proof end;

theorem Th30: :: ASYMPT_0:30

for b₁, b₂, b₃ being eventually-nonnegative Real_Sequence st b₁ in Big_Theta b₂ & b₂ in Big_Theta b₃ holds
b₁ in Big_Theta b₃

proof end;

theorem Th31: :: ASYMPT_0:31

for b₁, b₂ being positive Real_Sequence holds
( b₂ in Big_Theta b₁ iff ex b₃, b₄ being Real st
( b₃ > 0 & b₄ > 0 & ( for b₅ being Nat holds
( b₄ * (b₁ . b₅) <= b₂ . b₅ & b₂ . b₅ <= b₃ * (b₁ . b₅) ) ) ) )

proof end;

theorem Th32: :: ASYMPT_0:32

for b₁, b₂ being eventually-nonnegative Real_Sequence holds Big_Theta (b₁ + b₂) = Big_Theta (max b₁,b₂)

proof end;

theorem Th33: :: ASYMPT_0:33

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) > 0 holds
b₁ in Big_Theta b₂

proof end;

theorem Th34: :: ASYMPT_0:34

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is convergent & lim (b₁ /" b₂) = 0 holds
( b₁ in Big_Oh b₂ & not b₁ in Big_Theta b₂ )

proof end;

theorem Th35: :: ASYMPT_0:35

for b₁, b₂ being eventually-positive Real_Sequence st b₁ /" b₂ is divergent_to+infty holds
( b₁ in Big_Omega b₂ & not b₁ in Big_Theta b₂ )

proof end;

definition

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be set ;
func Big_Oh c₁,c₂ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 15
{ b₁ where B is Element of Funcs NAT ,REAL : ex b₁ being Realex b₂ being Nat st
( b₂ > 0 & ( for b₃ being Nat st b₄ >= b₃ & b₄ in a₂ holds
( b₁ . b₄ <= b₂ * (a₁ . b₄) & b₁ . b₄ >= 0 ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def15 defines Big_Oh ASYMPT_0:def 15 :

definition

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be set ;
func Big_Omega c₁,c₂ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 16
{ b₁ where B is Element of Funcs NAT ,REAL : ex b₁ being Realex b₂ being Nat st
( b₂ > 0 & ( for b₃ being Nat st b₄ >= b₃ & b₄ in a₂ holds
( b₁ . b₄ >= b₂ * (a₁ . b₄) & b₁ . b₄ >= 0 ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def16 defines Big_Omega ASYMPT_0:def 16 :

definition

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be set ;
func Big_Theta c₁,c₂ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 17
{ b₁ where B is Element of Funcs NAT ,REAL : ex b₁, b₂ being Realex b₃ being Nat st
( b₂ > 0 & b₃ > 0 & ( for b₄ being Nat st b₅ >= b₄ & b₅ in a₂ holds
( b₃ * (a₁ . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * (a₁ . b₅) ) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def17 defines Big_Theta ASYMPT_0:def 17 :

theorem Th36: :: ASYMPT_0:36

for b₁ being eventually-nonnegative Real_Sequence
for b₂ being set holds Big_Theta b₁,b₂ = (Big_Oh b₁,b₂) /\ (Big_Omega b₁,b₂)

proof end;

definition

let c₁ be Real_Sequence;
let c₂ be Nat;
func c₁ taken_every c₂ -> Real_Sequence means :Def18: :: ASYMPT_0:def 18
for b₁ being Nat holds a₃ . b₁ = a₁ . (a₂ * b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines taken_every ASYMPT_0:def 18 :

definition

let c₁ be eventually-nonnegative Real_Sequence;
let c₂ be Nat;
pred c₁ is_smooth_wrt c₂ means :Def19: :: ASYMPT_0:def 19
( a₁ is eventually-nondecreasing & a₁ taken_every a₂ in Big_Oh a₁ );

end;

:: deftheorem Def19 defines is_smooth_wrt ASYMPT_0:def 19 :

definition

let c₁ be eventually-nonnegative Real_Sequence;
attr a₁ is smooth means :Def20: :: ASYMPT_0:def 20
for b₁ being Nat st b₁ >= 2 holds
a₁ is_smooth_wrt b₁;

end;

:: deftheorem Def20 defines smooth ASYMPT_0:def 20 :

theorem Th37: :: ASYMPT_0:37

for b₁ being eventually-nonnegative Real_Sequence st ex b₂ being Nat st
( b₂ >= 2 & b₁ is_smooth_wrt b₂ ) holds
b₁ is smooth

proof end;

theorem Th38: :: ASYMPT_0:38

for b₁ being eventually-nonnegative Real_Sequence
for b₂ being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b₃ being Nat st b₁ is smooth & b₃ >= 2 & b₂ in Big_Oh b₁,{ (b₃ |^ b₄) where B is Nat : verum } holds
b₂ in Big_Oh b₁

proof end;

theorem Th39: :: ASYMPT_0:39

for b₁ being eventually-nonnegative Real_Sequence
for b₂ being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b₃ being Nat st b₁ is smooth & b₃ >= 2 & b₂ in Big_Omega b₁,{ (b₃ |^ b₄) where B is Nat : verum } holds
b₂ in Big_Omega b₁

proof end;

theorem Th40: :: ASYMPT_0:40

for b₁ being eventually-nonnegative Real_Sequence
for b₂ being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b₃ being Nat st b₁ is smooth & b₃ >= 2 & b₂ in Big_Theta b₁,{ (b₃ |^ b₄) where B is Nat : verum } holds
b₂ in Big_Theta b₁

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FUNCTION_DOMAIN of c₁, REAL ;
func c₂ + c₃ -> FUNCTION_DOMAIN of a₁, REAL equals :: ASYMPT_0:def 21
{ b₁ where B is Element of Funcs a₁,REAL : ex b₁, b₂ being Element of Funcs a₁,REAL st
( b₂ in a₂ & b₃ in a₃ & ( for b₃ being Element of a₁ holds b₁ . b₄ = (b₂ . b₄) + (b₃ . b₄) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def21 defines + ASYMPT_0:def 21 :

definition

let c₁ be non empty set ;
let c₂, c₃ be FUNCTION_DOMAIN of c₁, REAL ;
func max c₂,c₃ -> FUNCTION_DOMAIN of a₁, REAL equals :: ASYMPT_0:def 22
{ b₁ where B is Element of Funcs a₁,REAL : ex b₁, b₂ being Element of Funcs a₁,REAL st
( b₂ in a₂ & b₃ in a₃ & ( for b₃ being Element of a₁ holds b₁ . b₄ = max (b₂ . b₄),(b₃ . b₄) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def22 defines max ASYMPT_0:def 22 :

theorem Th41: :: ASYMPT_0:41

for b₁, b₂ being eventually-nonnegative Real_Sequence holds (Big_Oh b₁) + (Big_Oh b₂) = Big_Oh (b₁ + b₂)

proof end;

theorem Th42: :: ASYMPT_0:42

for b₁, b₂ being eventually-nonnegative Real_Sequence holds max (Big_Oh b₁),(Big_Oh b₂) = Big_Oh (max b₁,b₂)

proof end;

definition

let c₁, c₂ be FUNCTION_DOMAIN of NAT , REAL ;
func c₁ to_power c₂ -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 23
{ b₁ where B is Element of Funcs NAT ,REAL : ex b₁, b₂ being Element of Funcs NAT ,REAL ex b₃ being Element of NAT st
( b₂ in a₁ & b₃ in a₂ & ( for b₄ being Element of NAT st b₅ >= b₄ holds
b₁ . b₅ = (b₂ . b₅) to_power (b₃ . b₅) ) ) } ;
coherence

proof end;

end;

:: deftheorem Def23 defines to_power ASYMPT_0:def 23 :