CSSPACE3

:: CSSPACE3 semantic presentation

definition

func the_set_of_l1ComplexSequences -> ( ( ) ( ) Subset of ) means :: CSSPACE3:def 1
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) CUNITSTR ) iff ( x : ( ( ) ( ) set ) in the_set_of_ComplexSequences : ( ( non empty ) ( non empty ) set ) & seq_id x : ( ( ) ( ) set ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) is absolutely_summable ) );

end;

theorem :: CSSPACE3:1

for c being ( ( V33() ) ( V33() ) Complex)
for seq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence)
for rseq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Real_Sequence) st seq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) is convergent & ( for i being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Real_Sequence) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = |.((seq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V33() ) Element of COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) - c : ( ( V33() ) ( V33() ) Complex) ) : ( ( ) ( V33() ) set ) .| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) holds
( rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Real_Sequence) is convergent & lim rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Real_Sequence) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = |.((lim seq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) ) : ( ( ) ( V33() ) Element of COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) - c : ( ( V33() ) ( V33() ) Complex) ) : ( ( ) ( V33() ) set ) .| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ;

registration

cluster the_set_of_l1ComplexSequences : ( ( ) ( ) Subset of ) -> non empty ;

end;

registration

cluster the_set_of_l1ComplexSequences : ( ( ) ( non empty ) Subset of ) -> linearly-closed ;

end;

definition

func cl_norm -> ( ( Function-like V18( the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) V18( the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Function of the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) means :: CSSPACE3:def 2
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = Sum |.(seq_id x : ( ( ) ( ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non empty V38() V39() V40() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ;

end;

registration

let X be ( ( non empty ) ( non empty ) set ) ;
let Z be ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ;
let A be ( ( Function-like V18([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) V18([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) BinOp of X : ( ( non empty ) ( non empty ) set ) ) ;
let M be ( ( Function-like V18([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) V18([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) Function of [:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ;
let N be ( ( Function-like V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14(X : ( ( non empty ) ( non empty ) set ) ) V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ;

cluster CNORMSTR(# X : ( ( non empty ) ( non empty ) set ) ,Z : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,A : ( ( Function-like V18([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) V18([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,M : ( ( Function-like V18([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) V18([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,N : ( ( Function-like V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14(X : ( ( non empty ) ( non empty ) set ) ) V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non empty V38() V39() V40() ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) CNORMSTR ) -> non empty strict ;

end;

theorem :: CSSPACE3:2

for l being ( ( ) ( ) CNORMSTR ) st CLSStruct(# the carrier of l : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) , the ZeroF of l : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) , the addF of l : ( ( ) ( ) CNORMSTR ) : ( ( Function-like V18([: the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the Mult of l : ( ( ) ( ) CNORMSTR ) : ( ( Function-like V18([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) ) ( Relation-like [:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) -valued Function-like V18([:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) ) Element of bool [:[:COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) CLSStruct ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) holds
l : ( ( ) ( ) CNORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ComplexLinearSpace) ;

theorem :: CSSPACE3:3

for cseq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds cseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V33() ) Element of COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) = 0c : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V64() V65() V66() V67() V68() V69() V70() ) Element of COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) holds
( cseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) is absolutely_summable & Sum |.cseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non empty V38() V39() V40() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: CSSPACE3:4

for cseq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) st cseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) is absolutely_summable & Sum |.cseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non empty V38() V39() V40() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds cseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V33() ) Element of COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) = 0c : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V64() V65() V66() V67() V68() V69() V70() ) Element of COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ;

theorem :: CSSPACE3:6

( the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) = the_set_of_l1ComplexSequences : ( ( ) ( non empty linearly-closed ) Subset of ) & ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) is ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Complex_Sequence) & seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) is absolutely_summable ) ) ) & 0. Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V87( Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = CZeroseq : ( ( ) ( ) Element of the_set_of_ComplexSequences : ( ( non empty ) ( non empty ) set ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) + (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for p being ( ( V33() ) ( V33() ) Complex)
for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = p : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) (#) (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) & seq_id (- u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ( for u, v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) - (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) is absolutely_summable ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds ||.v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = Sum |.(seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) ) V38() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,COMPLEX : ( ( ) ( non empty V52() V64() V70() ) set ) :] : ( ( ) ( non empty V38() ) set ) : ( ( ) ( non empty ) set ) ) .| : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non empty V38() V39() V40() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ) ;

theorem :: CSSPACE3:7

for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for p being ( ( V33() ) ( V33() ) Complex) holds
( ( ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V87( Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( V87( Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) ) ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) & ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) + ||.y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) & ||.(p : ( ( V33() ) ( V33() ) Complex) * x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of Complex_l1_Space : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) = |.p : ( ( V33() ) ( V33() ) Complex) .| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ) ;

definition

let X be ( ( non empty ) ( non empty ) CNORMSTR ) ;
let x, y be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

func dist (x,y) -> ( ( ) ( V33() real ext-real ) Real) equals :: CSSPACE3:def 4
||.(x : ( ( ) ( ) set ) - y : ( ( Function-like V18([:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like non empty V14([:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ) V18([:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V33() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) ) ;

end;

definition

let CNRM be ( ( non empty ) ( non empty ) CNORMSTR ) ;
let seqt be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of CNRM : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of CNRM : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of CNRM : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

attr seqt is CCauchy means :: CSSPACE3:def 5
for r1 being ( ( ) ( V33() real ext-real ) Real) st r1 : ( ( ) ( V33() real ext-real ) Real) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() V70() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex k1 being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) st
for n1, m1 being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) st n1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) >= k1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) & m1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) >= k1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
dist ((seqt : ( ( ) ( ) set ) . n1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of CNRM : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(seqt : ( ( ) ( ) set ) . m1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V50() V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of CNRM : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V33() real ext-real ) Real) < r1 : ( ( ) ( V33() real ext-real ) Real) ;

end;

notation

let CNRM be ( ( non empty ) ( non empty ) CNORMSTR ) ;
let seq be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of CNRM : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of CNRM : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V52() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of CNRM : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
synonym Cauchy_sequence_by_Norm seq for CCauchy ;

end;