for a, b being ( ( real ) ( V11() real ext-real ) number )
for c being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds (a : ( ( real ) ( V11() real ext-real ) number ) / b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) to_power c : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) = (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) / (b : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

for a being ( ( real ) ( V11() real ext-real ) number )
for b, c being ( ( integer ) ( V11() real ext-real integer ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power (b : ( ( integer ) ( V11() real ext-real integer ) number ) + c : ( ( integer ) ( V11() real ext-real integer ) number ) ) : ( ( ) ( V11() real ext-real integer ) set ) : ( ( real ) ( V11() real ext-real ) set ) = (a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( integer ) ( V11() real ext-real integer ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) * (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( integer ) ( V11() real ext-real integer ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat)
for a being ( ( real ) ( V11() real ext-real ) number ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is even & a : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
(- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) = a : ( ( real ) ( V11() real ext-real ) number ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat)
for a being ( ( real ) ( V11() real ext-real ) number ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is odd & a : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
(- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) = - (a : ( ( real ) ( V11() real ext-real ) number ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( V11() ) ( V11() real ext-real ) set ) ;

abs tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of REAL : ( ( ) ( ) set ) ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat)
for r being ( ( non empty real ) ( non empty V11() real ext-real ) number ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is even holds
r : ( ( non empty real ) ( non empty V11() real ext-real ) number ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat)
for r being ( ( real ) ( V11() real ext-real ) number ) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is odd & r : ( ( real ) ( V11() real ext-real ) number ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
r : ( ( real ) ( V11() real ext-real ) number ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat)
for r being ( ( real ) ( V11() real ext-real ) number ) st m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is odd & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) & r : ( ( real ) ( V11() real ext-real ) number ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & r : ( ( real ) ( V11() real ext-real ) number ) > - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( V11() ) ( non empty V11() real ext-real non positive negative integer ) set ) holds
r : ( ( real ) ( V11() real ext-real ) number ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) >= r : ( ( real ) ( V11() real ext-real ) number ) to_power m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) ;

for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is odd & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds
tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) >= tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) ;

for n, m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is even & m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is even & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds
tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) <= tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) ;

for m, n being ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) st m : ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) >= n : ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) holds
Lucas m : ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) >= Lucas n : ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) holds tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power n : ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) > tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( non empty natural ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) > 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
- (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( non empty V11() real ext-real non positive negative ) Element of COMPLEX : ( ( ) ( ) set ) ) < tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) > 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) >= - (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( real ) ( V11() real ext-real ) set ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds
( ((tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) + (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) > 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & ((tau_bar : ( ( real ) ( non empty V11() real ext-real non positive negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) + (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds [\(((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) + (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) = Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
[/(((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) - (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) = Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) <> 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
[\((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) = Fib (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds [/((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer non even ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) / (sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) = Fib ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer non even ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is even holds
Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) * (Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) set ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is odd holds
Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [/((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) * (Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) set ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((((Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + ((sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) * (Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [/((((Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + ((sqrt 5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( ) set ) ) * (Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) holds Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = ((Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + (sqrt ((5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * ((Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ^2) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) set ) + (4 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * ((- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V11() ) ( non empty V11() real ext-real non positive negative integer ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((((Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) + (sqrt (((5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * ((Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ^2) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) set ) - (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * (Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) ) : ( ( ) ( V11() real ext-real integer ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real integer ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) * ((Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) set ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) set ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n, k being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st ( ( n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) & k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) > 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) or ( k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) > k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) ) holds
[\(((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) * (Fib n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) = Fib (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) + (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [/((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) - (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Lucas (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [/(tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Lucas ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer non even ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\(tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) to_power ((2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer non even ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is odd holds
Lucas (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) * (Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty V11() real ext-real positive non negative ) set ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) is even holds
Lucas (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [/((tau : ( ( real ) ( non empty V11() real ext-real positive non negative ) set ) * (Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) set ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) \] : ( ( integer ) ( V11() real ext-real integer ) set ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) <> 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Lucas (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = ((Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + (sqrt (5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * (((Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ^2) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) - (4 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * ((- 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( V11() ) ( non empty V11() real ext-real non positive negative integer ) set ) to_power n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) ;

for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) st n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) >= 4 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) holds
Lucas (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) = [\((((Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) set ) + (sqrt (((5 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * ((Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ^2) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) set ) - (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) * (Lucas n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer even ) set ) ) : ( ( ) ( V11() real ext-real integer ) set ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real integer ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( ) set ) ) /] : ( ( integer ) ( V11() real ext-real integer ) set ) ;