RSSPACE3

:: RSSPACE3 semantic presentation

definition

func the_set_of_l1RealSequences -> ( ( ) ( ) Subset of ) means :: RSSPACE3:def 1
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) NORMSTR ) iff ( x : ( ( ) ( ) set ) in the_set_of_RealSequences : ( ( non empty ) ( non empty ) set ) & seq_id x : ( ( ) ( ) set ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) is absolutely_summable ) );

end;

theorem :: RSSPACE3:1

for c being ( ( ) ( ext-real V36() real ) Real)
for seq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) st seq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) is convergent holds
for rseq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) st ( for i being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) holds rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) . i : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = abs ((seq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) . i : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) - c : ( ( ) ( ext-real V36() real ) Real) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) holds
( rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) is convergent & lim rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = abs ((lim seq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) - c : ( ( ) ( ext-real V36() real ) Real) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ;

registration

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

end;

registration

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

end;

definition

func l_norm -> ( ( Function-like V18( the_set_of_l1RealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like the_set_of_l1RealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( the_set_of_l1RealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) ) V18( the_set_of_l1RealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Function of the_set_of_l1RealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) means :: RSSPACE3:def 2
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the_set_of_l1RealSequences : ( ( ) ( non empty linearly-closed ) Subset of ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = Sum (abs (seq_id x : ( ( ) ( ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) 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 ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V14([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) BinOp of X : ( ( non empty ) ( non empty ) set ) ) ;
let M be ( ( Function-like V18([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V14([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) Function of [:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ;
let N be ( ( Function-like V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14(X : ( ( non empty ) ( non empty ) set ) ) V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ;

cluster NORMSTR(# 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 ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V14([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,M : ( ( Function-like V18([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like V14([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ) V18([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,N : ( ( Function-like V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14(X : ( ( non empty ) ( non empty ) set ) ) V18(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) -> non empty strict ;

end;

theorem :: RSSPACE3:2

for l being ( ( ) ( ) NORMSTR ) st RLSStruct(# the carrier of l : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) , the ZeroF of l : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) , the addF of l : ( ( ) ( ) NORMSTR ) : ( ( Function-like V18([: the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) -valued Function-like V18([: the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) , the Mult of l : ( ( ) ( ) NORMSTR ) : ( ( Function-like V18([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of b₁ : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) RLSStruct ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) holds
l : ( ( ) ( ) NORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() ) RealLinearSpace) ;

theorem :: RSSPACE3:3

for rseq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) st ( for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) holds rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) holds
( rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) is absolutely_summable & Sum (abs rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: RSSPACE3:4

for rseq being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) st rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) is absolutely_summable & Sum (abs rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) holds
for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) holds rseq : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: RSSPACE3:6

( the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) = the_set_of_l1RealSequences : ( ( ) ( 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 V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Real_Sequence) & seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) is absolutely_summable ) ) ) & 0. l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V84( l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = Zeroseq : ( ( ) ( ) Element of the_set_of_RealSequences : ( ( 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 V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) 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 l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) + (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) ) & ( for r being ( ( ) ( ext-real V36() real ) Real)
for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds r : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) (#) (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) ) & ( for u being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( - u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) & seq_id (- u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) = - (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) 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 l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id u : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) - (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) 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 V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) is absolutely_summable ) & ( for v being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds ||.v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = Sum (abs (seq_id v : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) V38() V39() V40() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) :] : ( ( ) ( V38() V39() V40() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ) ;

theorem :: RSSPACE3:7

for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( ext-real V36() real ) Real) holds
( ( ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V84( l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V84( l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) & 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) & ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) + ||.y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) & ||.(a : ( ( ) ( ext-real V36() real ) Real) * x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of l1_Space : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) = (abs a : ( ( ) ( ext-real V36() real ) Real) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ) ;

definition

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

func dist (x,y) -> ( ( ) ( ext-real V36() real ) Real) equals :: RSSPACE3:def 4
||.(x : ( ( non empty ) ( non empty ) 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 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 ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) ) ;

end;

definition

let NRM be ( ( non empty ) ( non empty ) NORMSTR ) ;
let seqt be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , the carrier of NRM : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of NRM : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) , the carrier of NRM : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;

attr seqt is CCauchy means :: RSSPACE3:def 5
for r1 being ( ( ) ( ext-real V36() real ) Real) st r1 : ( ( ) ( ext-real V36() real ) Real) > 0 : ( ( ) ( empty ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) holds
ex k1 being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) st
for n1, m1 being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) st n1 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) >= k1 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) & m1 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) >= k1 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) holds
dist ((seqt : ( ( non empty ) ( non empty ) set ) . n1 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of NRM : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(seqt : ( ( non empty ) ( non empty ) set ) . m1 : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V50() V56() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() ) Element of bool REAL : ( ( ) ( non empty V51() V57() V58() V59() V63() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of NRM : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real V36() real ) Real) < r1 : ( ( ) ( ext-real V36() real ) Real) ;

end;

notation

end;