:: LP_SPACE semantic presentation

begin

definition
let x be ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ;
let p be ( ( ) ( V11() real ext-real ) Real) ;
func x rto_power p -> ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) means :: LP_SPACE:def 1
 for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( Function-like V30([:x : ( ( ) ( ) NORMSTR ) ,x : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) ,x : ( ( ) ( ) NORMSTR ) ) ) ( Relation-like [:x : ( ( ) ( ) NORMSTR ) ,x : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) -defined x : ( ( ) ( ) NORMSTR ) -valued Function-like V30([:x : ( ( ) ( ) NORMSTR ) ,x : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) ,x : ( ( ) ( ) NORMSTR ) ) ) Element of bool [:[:x : ( ( ) ( ) NORMSTR ) ,x : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) ,x : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = (abs (x : ( ( ) ( ) NORMSTR ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power p : ( ( ) ( ) Element of x : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ;
end;

definition
let p be ( ( ) ( V11() real ext-real ) Real) ;
assume p : ( ( ) ( V11() real ext-real ) Real) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func the_set_of_RealSequences_l^ p -> ( ( non empty ) ( non empty ) Subset of ) means :: LP_SPACE:def 2
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of p : ( ( ) ( ) NORMSTR ) ) iff ( x : ( ( ) ( ) set ) in the_set_of_RealSequences : ( ( non empty ) ( non empty ) set ) & (seq_id x : ( ( ) ( ) set ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( ) NORMSTR ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable ) );
end;

theorem :: LP_SPACE:1
for a, b, c being ( ( ) ( V11() real ext-real ) Real) st a : ( ( ) ( V11() real ext-real ) Real) >= 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) & a : ( ( ) ( V11() real ext-real ) Real) < b : ( ( ) ( V11() real ext-real ) Real) & c : ( ( ) ( V11() real ext-real ) Real) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
a : ( ( ) ( V11() real ext-real ) Real) to_power c : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) < b : ( ( ) ( V11() real ext-real ) Real) to_power c : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ;

theorem :: LP_SPACE:2
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
for a, b being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence)
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((Partial_Sums ((a : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) + b : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) <= (((Partial_Sums (a : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) + (((Partial_Sums (b : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ;

theorem :: LP_SPACE:3
for a, b being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence)
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) & a : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable & b : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable holds
( (a : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) + b : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable & (Sum ((a : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) + b : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) <= ((Sum (a : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) + ((Sum (b : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ;

theorem :: LP_SPACE:4
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) is linearly-closed ;

theorem :: LP_SPACE:5
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is ( ( ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) Subspace of Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) ) ;

theorem :: LP_SPACE:6
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
( RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is Abelian & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is add-associative & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is right_zeroed & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is right_complementable & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is vector-distributive & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is scalar-distributive & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is scalar-associative & RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RLSStruct ) is scalar-unital ) ;

theorem :: LP_SPACE:7
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
RLSStruct(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty 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 zeroed ) RealLinearSpace) ;

definition
let p be ( ( ) ( V11() real ext-real ) Real) ;
func l_norm^ p -> ( ( Function-like V30( the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) means :: LP_SPACE:def 3
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) holds
it : ( ( ) ( ) Element of p : ( ( ) ( ) NORMSTR ) ) . x : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = (Sum ((seq_id x : ( ( ) ( ) set ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( ) NORMSTR ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ;
end;

theorem :: LP_SPACE:8
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) 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 zeroed ) RealLinearSpace) ;

theorem :: LP_SPACE:9
for p being ( ( ) ( V11() real ext-real ) Real) st p : ( ( ) ( V11() real ext-real ) Real) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) is ( ( ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) Subspace of Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) ) ;

begin

theorem :: LP_SPACE:10
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
for lp being ( ( non empty ) ( non empty ) NORMSTR ) st lp : ( ( non empty ) ( non empty ) NORMSTR ) = NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) holds
( the carrier of lp : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) = the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) 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 V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) & (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable ) ) ) & 0. lp : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V79(b2 : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = Zeroseq : ( ( ) ( ) Element of the_set_of_RealSequences : ( ( non empty ) ( non empty ) set ) ) & ( for x being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) = seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for x, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) + (seq_id y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for r being ( ( ) ( V11() real ext-real ) Real)
for x being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds r : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = r : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) (#) (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for x being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds
( - x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = - (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) & seq_id (- x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) = - (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & ( for x, y being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) - (seq_id y : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) & ( for x being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds (seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable ) & ( for x being ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) holds ||.x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = (Sum ((seq_id x : ( ( ) ( ) VECTOR of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ) ;

theorem :: LP_SPACE:11
for p being ( ( ) ( V11() real ext-real ) Real) st p : ( ( ) ( V11() real ext-real ) Real) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for rseq being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds rseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) holds
( rseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable & (Sum (rseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: LP_SPACE:12
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
for rseq being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) st rseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) is summable & (Sum (rseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) rto_power p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) to_power (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) / p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) number ) holds rseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Real_Sequence) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: LP_SPACE:13
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
for lp being ( ( non empty ) ( non empty ) NORMSTR ) st lp : ( ( non empty ) ( non empty ) NORMSTR ) = NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) holds
for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for a being ( ( ) ( V11() real ext-real ) Real) holds
( ( ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) implies x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. lp : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V79(b2 : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = 0. lp : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( V79(b2 : ( ( non empty ) ( non empty ) NORMSTR ) ) ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) implies ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) ) & 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V45() V46() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) & ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) + ||.y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) & ||.(a : ( ( ) ( V11() real ext-real ) Real) * x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) = (abs a : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ;

theorem :: LP_SPACE:14
for p being ( ( ) ( V11() real ext-real ) Real) st p : ( ( ) ( V11() real ext-real ) Real) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for lp being ( ( non empty ) ( non empty ) NORMSTR ) st lp : ( ( non empty ) ( non empty ) NORMSTR ) = NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) holds
( lp : ( ( non empty ) ( non empty ) NORMSTR ) is reflexive & lp : ( ( non empty ) ( non empty ) NORMSTR ) is discerning & lp : ( ( non empty ) ( non empty ) NORMSTR ) is RealNormSpace-like ) ;

theorem :: LP_SPACE:15
for p being ( ( ) ( V11() real ext-real ) Real) st p : ( ( ) ( V11() real ext-real ) Real) >= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for lp being ( ( non empty ) ( non empty ) NORMSTR ) st lp : ( ( non empty ) ( non empty ) NORMSTR ) = NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) holds
lp : ( ( non empty ) ( non empty ) NORMSTR ) is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) ;

theorem :: LP_SPACE:16
for p being ( ( ) ( V11() real ext-real ) Real) st 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) holds
for lp being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) st lp : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) = NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( V11() real ext-real ) Real) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ b1 : ( ( ) ( V11() real ext-real ) Real) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) holds
for vseq being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st vseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is Cauchy_sequence_by_Norm holds
vseq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V26( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

definition
let p be ( ( ) ( V11() real ext-real ) Real) ;
assume 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() ) Element of bool REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) : ( ( ) ( non empty ) set ) ) ) <= p : ( ( ) ( V11() real ext-real ) Real) ;
func l_Space^ p -> ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like V165() ) ( non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like V165() ) RealBanachSpace) equals :: LP_SPACE:def 4
 NORMSTR(# (the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(Zero_ ((the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( ) ( ) Element of the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) ,(Add_ ((the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Mult_ ((the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) ,Linear_Space_of_RealSequences : ( ( ) ( non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed ) RLSStruct ) )) : ( ( Function-like V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) -defined the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) -valued Function-like V26([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ) V30([:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) , the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) ,(the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) ) : ( ( non empty ) ( non empty ) Subset of ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(l_norm^ p : ( ( ) ( ) NORMSTR ) ) : ( ( Function-like V30( the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) ) ( non empty Relation-like the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) -defined REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) -valued Function-like V26( the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) ) V30( the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) V33() V34() V35() ) Function of the_set_of_RealSequences_l^ p : ( ( ) ( ) NORMSTR ) : ( ( non empty ) ( non empty ) Subset of ) , REAL : ( ( ) ( non empty V47() V52() V53() V54() V58() ) set ) ) #) : ( ( strict ) ( strict ) NORMSTR ) ;
end;