:: HOLDER_1 semantic presentation
begin
registration
let
x
be ( (
real
) (
V22
()
real
ext-real
)
number
) ;
cluster
right_closed_halfline
x
: ( (
real
) (
V22
()
real
ext-real
)
set
) : ( ( ) (
V49
()
V72
()
V73
()
V74
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
->
non
empty
;
end;
theorem
:: HOLDER_1:1
for
p
,
q
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
*
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
(
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
+
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ;
theorem
:: HOLDER_1:2
for
p
,
q
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
(
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ;
theorem
:: HOLDER_1:3
for
p
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
,
b
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
<=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ;
theorem
:: HOLDER_1:4
for
p
,
q
,
a
,
b
being ( ( ) (
V22
()
real
ext-real
)
Real
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
a
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) & (
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) implies
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) & (
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) implies
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
#R
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) ;
theorem
:: HOLDER_1:5
for
p
,
q
,
a
,
b
being ( ( ) (
V22
()
real
ext-real
)
Real
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) & (
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) implies
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) & (
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) implies
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
*
b
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
(
a
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
b
: ( ( ) (
V22
()
real
ext-real
)
Real
)
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) ;
begin
theorem
:: HOLDER_1:6
for
p
,
q
being ( ( ) (
V22
()
real
ext-real
)
Real
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
for
a
,
b
,
ap
,
bq
,
ab
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
bq
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
abs
(
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
*
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) holds
for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
Partial_Sums
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
(
(
Partial_Sums
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
*
(
(
(
Partial_Sums
bq
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ;
theorem
:: HOLDER_1:7
for
p
being ( ( ) (
V22
()
real
ext-real
)
Real
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
,
b
,
ap
,
bp
,
ab
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
bp
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) holds
for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
Partial_Sums
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
(
(
Partial_Sums
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
(
Partial_Sums
bp
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ;
theorem
:: HOLDER_1:8
for
a
,
b
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) &
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
V41
() holds
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
lim
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
lim
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ;
theorem
:: HOLDER_1:9
for
a
,
b
,
c
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
c
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) &
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
c
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
V41
() holds
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
lim
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
lim
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
lim
c
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ;
theorem
:: HOLDER_1:10
for
p
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
,
ap
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
& ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) & ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) holds
(
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
lim
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
lim
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ;
theorem
:: HOLDER_1:11
for
p
being ( ( ) (
V22
()
real
ext-real
)
Real
) st
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
,
ap
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
& ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
V22
()
real
ext-real
non
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) & ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
(
Partial_Sums
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Element
of
K19
(
K20
(
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ,
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
complex-valued
ext-real-valued
real-valued
)
set
) ) : ( ( ) ( )
set
) )
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) holds
(
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
convergent
&
lim
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
Sum
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
V41
() & ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
Sum
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) ;
theorem
:: HOLDER_1:12
for
p
,
q
being ( ( ) (
V22
()
real
ext-real
)
Real
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) &
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
for
a
,
b
,
ap
,
bq
,
ab
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
bq
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
q
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
abs
(
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
*
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) &
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
&
bq
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
holds
(
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
&
Sum
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
(
Sum
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
*
(
(
Sum
bq
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
q
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ;
theorem
:: HOLDER_1:13
for
p
being ( ( ) (
V22
()
real
ext-real
)
Real
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
<
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) holds
for
a
,
b
,
ap
,
bp
,
ab
being ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) st ( for
n
being ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
bp
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) &
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
=
(
abs
(
(
a
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
b
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
.
n
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
p
: ( ( ) (
V22
()
real
ext-real
)
Real
) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ) &
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
&
bp
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
holds
(
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
) is
summable
&
(
Sum
ab
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
<=
(
(
Sum
ap
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
+
(
(
Sum
bp
: ( (
V6
()
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) )
-defined
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
)
-valued
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
)
Real_Sequence
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
to_power
(
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V22
()
real
ext-real
positive
non
negative
V33
()
V66
()
V72
()
V73
()
V74
()
V75
()
V76
()
V77
() )
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V72
()
V73
()
V74
()
V75
()
V76
()
V77
()
V78
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) ( )
set
) ) )
/
p
: ( ( ) (
V22
()
real
ext-real
)
Real
)
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) )
)
: ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) : ( ( ) (
V22
()
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V67
()
V72
()
V73
()
V74
()
V78
() )
set
) ) ) ;