begin
begin
theorem
for
a,
b,
m,
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
( not
a : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
< b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) or
(modSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V35()
V36()
V37()
V38() )
sequence of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
. a : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> (modSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V35()
V36()
V37()
V38() )
sequence of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
. b : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) or
(modSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V35()
V36()
V37()
V38() )
sequence of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
. a : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) ;
begin
theorem
for
m,
n,
k being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(
(scf (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) / n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real non negative rational ) Element of COMPLEX : ( ( ) ( non zero V45() V70() V76() ) set ) ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. k : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= (divSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V35()
V36()
V37()
V38() )
sequence of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
. k : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) &
(rfs (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) / n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real non negative rational ) Element of COMPLEX : ( ( ) ( non zero V45() V70() V76() ) set ) ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
/ ((modSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V35() V36() V37() V38() ) sequence of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) . 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real non
negative rational )
Element of
COMPLEX : ( ( ) ( non
zero V45()
V70()
V76() )
set ) ) &
(rfs (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) / n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real non negative rational ) Element of COMPLEX : ( ( ) ( non zero V45() V70() V76() ) set ) ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. (k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= ((modSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V35() V36() V37() V38() ) sequence of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) . k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((modSeq (m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) )) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V35() V36() V37() V38() ) sequence of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) . (k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real non
negative rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ;
begin
definition
let r be ( (
real ) (
complex real ext-real )
number ) ;
func convergent_numerators r -> ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
means
(
it : ( ( ) ( )
set )
. 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= (scf r : ( ( ) ( ) set ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) &
it : ( ( ) ( )
set )
. 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= (((scf r : ( ( ) ( ) set ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((scf r : ( ( ) ( ) set ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
+ 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) & ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
it : ( ( ) ( )
set )
. (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= (((scf r : ( ( ) ( ) set ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * (it : ( ( ) ( ) set ) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
+ (it : ( ( ) ( ) set ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) );
end;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
>= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) holds
1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
/ (((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
< 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
/ (((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * (((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ^2) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
for
r being ( (
real ) (
complex real ext-real )
number ) holds
((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= ((((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) + ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) + ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
<> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
(((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) / ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
- (((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) / ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= ((- 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non positive integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ (((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
for
r being ( (
real ) (
complex real ext-real )
number ) holds
(((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
- (((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= ((- 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non positive integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
* ((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
<> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
(((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) / ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
- (((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) / ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= (((- 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real non positive integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ (((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
<> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
>= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) holds
((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= (((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) - ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ (((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) - ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
<> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
abs ((((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) / ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) - (((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) / ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
/ (abs (((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) * ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
(cocf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. 2 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= ((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
+ (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) / (((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) + (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) / ((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
(cocf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Real_Sequence)
. 3 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
= ((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 0 : ( ( ) ( zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer rational V70() V71() V72() V73() V74() V75() V76() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
+ (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) / (((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) + (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) / (((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) + (1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) / ((scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued INT : ( ( ) ( non zero V45() V70() V71() V72() V73() V74() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Integer_Sequence) . 3 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) ( complex real ext-real rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
>= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) holds
((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
< ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
>= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) holds
((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) - 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) - 2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;
theorem
for
r being ( (
real ) (
complex real ext-real )
number ) st ( for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) holds
(scf r : ( ( real ) ( complex real ext-real ) number ) ) : ( (
INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ) ( non
zero Relation-like NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set )
-valued INT : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V73()
V74()
V76() )
set )
-valued Function-like V26(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) )
V30(
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
V35()
V36()
V37() )
Integer_Sequence)
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) : ( ( ) (
complex real ext-real integer rational )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
> 0 : ( ( ) (
zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non
positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural complex real ext-real non
negative integer rational )
Nat)
>= 1 : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non
negative integer rational V70()
V71()
V72()
V73()
V74()
V75() )
Element of
NAT : ( ( ) ( non
zero epsilon-transitive epsilon-connected ordinal V70()
V71()
V72()
V73()
V74()
V75()
V76() )
Element of
K6(
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) ( )
set ) ) ) holds
((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . (2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
< ((c_n r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) )
/ ((c_d r : ( ( real ) ( complex real ext-real ) number ) ) : ( ( Function-like V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) -valued Function-like V26( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) V35() V36() V37() ) Real_Sequence) . ((2 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) - 1 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer rational V70() V71() V72() V73() V74() V75() ) Element of NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() ) Element of K6(REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex real ext-real integer rational ) Element of REAL : ( ( ) ( non zero V45() V70() V71() V72() V76() ) set ) ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) : ( ( ) (
complex real ext-real )
Element of
REAL : ( ( ) ( non
zero V45()
V70()
V71()
V72()
V76() )
set ) ) ;