( the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) = the_set_of_l2RealSequences : ( ( ) ( V11() V137( Linear_Space_of_RealSequences : ( ( ) ( V78() right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) ) ) Element of bool the carrier of Linear_Space_of_RealSequences : ( ( ) ( V78() right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) RLSStruct ) : ( ( ) ( V11() ) set ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) is ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) iff ( x : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) is ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) & (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) (#) (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) is summable ) ) ) & 0. l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V85( l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) ) ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) = Zeroseq : ( ( ) ( ) Element of the_set_of_RealSequences : ( ( V11() ) ( V11() ) set ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) = seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) + (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( V33() real ext-real ) Real)
for u being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds r : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) = r : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) (#) (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds
( - u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) & seq_id (- u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) - (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) ) & ( for v, w being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds
( (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) (#) (seq_id w : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) is summable & ( for v, w being ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) holds v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) .|. w : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) = Sum ((seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) (#) (seq_id w : ( ( ) ( ) VECTOR of ( ( ) ( V11() ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ) ) ) ;

for x, y, z being ( ( ) ( ) Point of ( ( ) ( V11() ) set ) )
for a being ( ( ) ( V33() real ext-real ) Real) holds
( ( x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) = 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V38() V57() V58() V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) = 0. l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V85( l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) ) ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) = 0. l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V85( l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) ) ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) implies x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) = 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V38() V57() V58() V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) ) & 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V38() V57() V58() V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) <= x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) & x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) = y : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) & (x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) .|. z : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) = (x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. z : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) + (y : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. z : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) & (a : ( ( ) ( V33() real ext-real ) Real) * x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( ) Element of the carrier of l2_Space : ( ( V78() ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) UNITSTR ) : ( ( ) ( V11() ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) = a : ( ( ) ( V33() real ext-real ) Real) * (x : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( V11() ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ;

mode RealHilbertSpace is ( ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like complete ) ( V78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like complete ) RealUnitarySpace) ;

for r being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) holds 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V38() V57() V58() V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) <= r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) holds
( ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) holds 0 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V38() V57() V58() V59() V60() V61() V62() V63() V64() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) <= (Partial_Sums r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) holds r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= (Partial_Sums r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) & ( r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) is summable implies ( ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) holds (Partial_Sums r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Element of bool [:NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) :] : ( ( ) ( V40() V41() V42() ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= Sum r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) holds r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= Sum r : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ) ) ) ;

( ( for x, y being ( ( ) ( V33() real ext-real ) Real) holds (x : ( ( ) ( V33() real ext-real ) Real) + y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) * (x : ( ( ) ( V33() real ext-real ) Real) + y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= ((2 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) * x : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) * x : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) + ((2 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) * y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) * y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) & ( for x, y being ( ( ) ( V33() real ext-real ) Real) holds x : ( ( ) ( V33() real ext-real ) Real) * x : ( ( ) ( V33() real ext-real ) Real) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= ((2 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) * (x : ( ( ) ( V33() real ext-real ) Real) - y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) * (x : ( ( ) ( V33() real ext-real ) Real) - y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) + ((2 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) * y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) * y : ( ( ) ( V33() real ext-real ) Real) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ) ;

for e being ( ( ) ( V33() real ext-real ) Real)
for s being ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) st s : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) is convergent & ex k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) st
for i being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) st k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) <= i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) holds
s : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real non negative V38() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= e : ( ( ) ( V33() real ext-real ) Real) holds
lim s : ( ( Function-like V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) ) ( Relation-like NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) -valued Function-like V11() V14( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V58() V59() V60() V61() V62() V63() V64() ) Element of bool REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) V40() V41() V42() ) Real_Sequence) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( V11() V52() V58() V59() V60() V64() ) set ) ) <= e : ( ( ) ( V33() real ext-real ) Real) ;