:: PRE_FF semantic presentation

begin

definition
let n be ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ;
func Fib n -> ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) means :: PRE_FF:def 1
 ex fib being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st
( it : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (fib : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) `1 : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & fib : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) . 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = [0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ) & ( for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) holds fib : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) . (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = [((fib : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) `2) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,(((fib : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) `1) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + ((fib : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11([:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,[:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty V7() V10( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) V11( REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) ) Element of bool [:REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ,REAL : ( ( ) ( V35() V36() V37() V41() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) `2) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ] : ( ( ) ( ) Element of [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: PRE_FF:1
( Fib 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & Fib 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) holds Fib ((n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (Fib n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + (Fib (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: PRE_FF:2
for i being ( ( integer ) ( ext-real V27() real integer ) Integer) holds i : ( ( integer ) ( ext-real V27() real integer ) Integer) div 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( integer ) ( ext-real V27() real integer ) set ) = i : ( ( integer ) ( ext-real V27() real integer ) Integer) ;

theorem :: PRE_FF:3
for i, j being ( ( integer ) ( ext-real V27() real integer ) Integer) st j : ( ( integer ) ( ext-real V27() real integer ) Integer) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & i : ( ( integer ) ( ext-real V27() real integer ) Integer) div j : ( ( integer ) ( ext-real V27() real integer ) Integer) : ( ( integer ) ( ext-real V27() real integer ) set ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
i : ( ( integer ) ( ext-real V27() real integer ) Integer) < j : ( ( integer ) ( ext-real V27() real integer ) Integer) ;

theorem :: PRE_FF:4
for i, j being ( ( integer ) ( ext-real V27() real integer ) Integer) st 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( integer ) ( ext-real V27() real integer ) Integer) & i : ( ( integer ) ( ext-real V27() real integer ) Integer) < j : ( ( integer ) ( ext-real V27() real integer ) Integer) holds
i : ( ( integer ) ( ext-real V27() real integer ) Integer) div j : ( ( integer ) ( ext-real V27() real integer ) Integer) : ( ( integer ) ( ext-real V27() real integer ) set ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PRE_FF:5
for i, j, k being ( ( integer ) ( ext-real V27() real integer ) Integer) st k : ( ( integer ) ( ext-real V27() real integer ) Integer) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
(i : ( ( integer ) ( ext-real V27() real integer ) Integer) div j : ( ( integer ) ( ext-real V27() real integer ) Integer) ) : ( ( integer ) ( ext-real V27() real integer ) set ) div k : ( ( integer ) ( ext-real V27() real integer ) Integer) : ( ( integer ) ( ext-real V27() real integer ) set ) = i : ( ( integer ) ( ext-real V27() real integer ) Integer) div (j : ( ( integer ) ( ext-real V27() real integer ) Integer) * k : ( ( integer ) ( ext-real V27() real integer ) Integer) ) : ( ( ) ( ext-real V27() real integer ) set ) : ( ( integer ) ( ext-real V27() real integer ) set ) ;

theorem :: PRE_FF:6
for i being ( ( integer ) ( ext-real V27() real integer ) Integer) holds
( i : ( ( integer ) ( ext-real V27() real integer ) Integer) mod 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( integer ) ( ext-real V27() real integer ) set ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) or i : ( ( integer ) ( ext-real V27() real integer ) Integer) mod 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( integer ) ( ext-real V27() real integer ) set ) = 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: PRE_FF:7
for i being ( ( integer ) ( ext-real V27() real integer ) Integer) st i : ( ( integer ) ( ext-real V27() real integer ) Integer) is ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
i : ( ( integer ) ( ext-real V27() real integer ) Integer) div 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( integer ) ( ext-real V27() real integer ) set ) is ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PRE_FF:8
for a, b, c being ( ( real ) ( ext-real V27() real ) number ) st a : ( ( real ) ( ext-real V27() real ) number ) <= b : ( ( real ) ( ext-real V27() real ) number ) & c : ( ( real ) ( ext-real V27() real ) number ) > 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
c : ( ( real ) ( ext-real V27() real ) number ) to_power a : ( ( real ) ( ext-real V27() real ) number ) : ( ( real ) ( ext-real V27() real ) set ) <= c : ( ( real ) ( ext-real V27() real ) number ) to_power b : ( ( real ) ( ext-real V27() real ) number ) : ( ( real ) ( ext-real V27() real ) set ) ;

theorem :: PRE_FF:9
for r, s being ( ( real ) ( ext-real V27() real ) number ) st r : ( ( real ) ( ext-real V27() real ) number ) >= s : ( ( real ) ( ext-real V27() real ) number ) holds
[\r : ( ( real ) ( ext-real V27() real ) number ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) >= [\s : ( ( real ) ( ext-real V27() real ) number ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) ;

theorem :: PRE_FF:10
for a, b, c being ( ( real ) ( ext-real V27() real ) number ) st a : ( ( real ) ( ext-real V27() real ) number ) > 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & b : ( ( real ) ( ext-real V27() real ) number ) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & c : ( ( real ) ( ext-real V27() real ) number ) >= b : ( ( real ) ( ext-real V27() real ) number ) holds
log (a : ( ( real ) ( ext-real V27() real ) number ) ,c : ( ( real ) ( ext-real V27() real ) number ) ) : ( ( real ) ( ext-real V27() real ) set ) >= log (a : ( ( real ) ( ext-real V27() real ) number ) ,b : ( ( real ) ( ext-real V27() real ) number ) ) : ( ( real ) ( ext-real V27() real ) set ) ;

theorem :: PRE_FF:11
for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
[\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,(2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V27() real integer ) set ) <> [\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) ;

theorem :: PRE_FF:12
for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
[\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,(2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V27() real integer ) set ) >= [\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) ;

theorem :: PRE_FF:13
for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
[\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,(2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) = [\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) ;

theorem :: PRE_FF:14
for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) > 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
[\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) )) : ( ( real ) ( ext-real V27() real ) set ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V27() real integer ) set ) = [\(log (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ,((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ext-real V27() real ) Element of REAL : ( ( ) ( V35() V36() V37() V41() ) set ) ) /] : ( ( integer ) ( ext-real V27() real integer ) set ) ;

definition
let f be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ;
let n be ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: .
redefine func f . n -> ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let n be ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ;
func Fusc n -> ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) means :: PRE_FF:def 2
it : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) if n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )
otherwise ex l being ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ex fusc being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) st
( l : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & it : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . l : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) /. n : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = <*1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() V49(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) holds
( ( for k being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * k : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( FinSequence-like ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ^ <*((fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( FinSequence-like ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) /. k : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() V49(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ( for k being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * k : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( FinSequence-like ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ^ <*(((fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( FinSequence-like ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) /. k : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + ((fusc : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) . n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( FinSequence-like ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) * : ( ( ) ( non empty functional FinSequence-membered ) M10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) )) ) /. (k : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) *> : ( ( ) ( non empty V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() V49(1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V7() V10( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) V11( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) Function-like V42() FinSequence-like FinSubsequence-like ) FinSequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ) );
end;

theorem :: PRE_FF:15
( Fusc 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & Fusc 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) holds
( Fusc (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = Fusc n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) & Fusc ((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (Fusc n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + (Fusc (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ) ;

theorem :: PRE_FF:16
for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) <> 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) < 2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PRE_FF:17
for n being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) holds n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) < (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PRE_FF:18
for A, B being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) holds B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) = (A : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc 0 : ( ( ) ( empty functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real integer V35() V36() V37() V38() V39() V40() V41() FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + (B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PRE_FF:19
for n, A, B, N being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st Fusc N : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc ((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + (B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc (((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
Fusc N : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + ((B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + A : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) set ) * (Fusc (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: PRE_FF:20
for n, A, B, N being ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) st Fusc N : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = (A : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc (2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + (B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc ((2 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
Fusc N : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) = ((A : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) set ) * (Fusc n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) + (B : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) * (Fusc (n : ( ( natural ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer ) Nat) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() real integer V35() V36() V37() V38() V39() V40() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V35() V36() V37() V38() V39() V40() V41() ) Element of bool REAL : ( ( ) ( V35() V36() V37() V41() ) set ) : ( ( ) ( non empty ) set ) ) ) ;