( the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) = the_set_of_l2ComplexSequences : ( ( ) ( ) Element of bool the carrier of Linear_Space_of_ComplexSequences : ( ( V80() strict ) ( V80() right_complementable V131() V132() V133() strict vector-distributive scalar-distributive scalar-associative scalar-unital ) L16()) : ( ( ) ( non zero ) set ) : ( ( ) ( non zero ) set ) ) & ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) iff ( x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) is ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) & |.(seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non zero V38() V39() V40() ) set ) : ( ( ) ( non zero ) set ) ) (#) |.(seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non zero V38() V39() V40() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non zero V38() V39() V40() ) set ) : ( ( ) ( non zero ) set ) ) is summable ) ) ) & ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non zero ) set ) ) iff ( x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) is ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) & (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) (#) ((seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) *') : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) is absolutely_summable ) ) ) & 0. Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( zero ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) = CZeroseq : ( ( ) ( ) Element of the_set_of_ComplexSequences : ( ( non zero ) ( non zero ) set ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) = seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) + (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ) & ( for r being ( ( complex ) ( complex ) Complex)
for u being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds r : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) = r : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) (#) (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds
( - u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) & seq_id (- u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) - (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ) & ( for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds
( |.(seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non zero V38() V39() V40() ) set ) : ( ( ) ( non zero ) set ) ) (#) |.(seq_id w : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non zero V38() V39() V40() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non zero V38() V39() V40() ) set ) : ( ( ) ( non zero ) set ) ) is summable & ( for v, w being ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) holds v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) .|. w : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) : ( ( complex ) ( complex ) set ) = Sum ((seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) (#) ((seq_id w : ( ( ) ( ) VECTOR of ( ( ) ( non zero ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) *') : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ) ) ) ;

for x, y, z being ( ( ) ( ) Point of ( ( ) ( non zero ) set ) )
for a being ( ( complex ) ( complex ) Complex) holds
( ( x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) : ( ( complex ) ( complex ) set ) = 0 : ( ( ) ( zero V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) = 0. Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( zero ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) = 0. Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( zero ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) : ( ( complex ) ( complex ) set ) = 0 : ( ( ) ( zero V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) ) & Re (x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) >= 0 : ( ( ) ( zero V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) & Im (x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) = 0 : ( ( ) ( zero V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) & x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) : ( ( complex ) ( complex ) set ) = (y : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( complex ) ( complex ) set ) *' : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) & (x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) .|. z : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) : ( ( complex ) ( complex ) set ) = (x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. z : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( complex ) ( complex ) set ) + (y : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. z : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex ) set ) & (a : ( ( complex ) ( complex ) Complex) * x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_l2_Space : ( ( V80() ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ) CUNITSTR ) : ( ( ) ( non zero ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) : ( ( complex ) ( complex ) set ) = a : ( ( complex ) ( complex ) Complex) * (x : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) .|. y : ( ( ) ( ) Point of ( ( ) ( non zero ) set ) ) ) : ( ( complex ) ( complex ) set ) : ( ( ) ( complex ) set ) ) ;

mode ComplexHilbertSpace is ( ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexUnitarySpace-like complete ) ( V80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexUnitarySpace-like complete ) ComplexUnitarySpace) ;

for z1, z2 being ( ( complex ) ( complex ) Complex) st (Re z1 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * (Im z2 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) = (Re z2 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * (Im z1 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) & ((Re z1 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * (Re z2 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) + ((Im z1 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * (Im z2 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) >= 0 : ( ( ) ( zero V26() V27() V28() V30() V31() V32() complex V34() ext-real non positive non negative V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) holds
|.(z1 : ( ( complex ) ( complex ) Complex) + z2 : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) = |.z1 : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) + |.z2 : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ;

for x, y being ( ( complex ) ( complex ) Complex) holds 2 : ( ( ) ( non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) * |.(x : ( ( complex ) ( complex ) Complex) * y : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) <= (|.x : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ^2) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) + (|.y : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ^2) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ;

for x, y being ( ( complex ) ( complex ) Complex) holds
( |.(x : ( ( complex ) ( complex ) Complex) + y : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * |.(x : ( ( complex ) ( complex ) Complex) + y : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) <= ((2 : ( ( ) ( non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) * |.x : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * |.x : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) + ((2 : ( ( ) ( non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) * |.y : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * |.y : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) & |.x : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * |.x : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) <= ((2 : ( ( ) ( non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) * |.(x : ( ( complex ) ( complex ) Complex) - y : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * |.(x : ( ( complex ) ( complex ) Complex) - y : ( ( complex ) ( complex ) Complex) ) : ( ( ) ( complex ) set ) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) + ((2 : ( ( ) ( non zero V26() V27() V28() V32() complex V34() ext-real positive non negative V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) * |.y : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) * |.y : ( ( complex ) ( complex ) Complex) .| : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( complex V34() ext-real ) Element of REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) ) ) ;

for seq being ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) holds Partial_Sums (seq : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) *') : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) = (Partial_Sums seq : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) ) : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) *' : ( ( Function-like V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) -defined COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) -valued Function-like non zero V14( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ) V18( NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) , COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non zero V26() V27() V28() V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non zero V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non zero ) set ) ) ,COMPLEX : ( ( ) ( non zero V52() V64() V70() ) set ) :] : ( ( ) ( non zero V38() ) set ) : ( ( ) ( non zero ) set ) ) ;