:: LP_SPACE semantic presentation

REAL is non empty V47() V52() V53() V54() V58() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V47() V52() V58() set
[:NAT,REAL:] is non empty V33() V34() V35() set
bool [:NAT,REAL:] is non empty set
RAT is non empty V47() V52() V53() V54() V55() V58() set
INT is non empty V47() V52() V53() V54() V55() V56() V58() set
omega is non empty epsilon-transitive epsilon-connected ordinal V52() V53() V54() V55() V56() V57() V58() set
bool omega is non empty set
bool NAT is non empty set
the_set_of_RealSequences is non empty set
[:the_set_of_RealSequences,the_set_of_RealSequences:] is non empty set
[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
[:REAL,the_set_of_RealSequences:] is non empty set
[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
Linear_Space_of_RealSequences is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of Linear_Space_of_RealSequences is non empty set
bool the carrier of Linear_Space_of_RealSequences is non empty set
the_set_of_l2RealSequences is non empty linearly-closed Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is non empty set
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is non empty V33() V34() V35() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is non empty set
the_set_of_l1RealSequences is Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l1RealSequences,REAL:] is V33() V34() V35() set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty V33() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V33() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V33() V34() V35() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V33() V34() V35() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V33() V34() V35() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V33() V34() V35() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V33() V34() V35() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V33() V34() V35() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() set
1 is 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
0 is 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
- 1 is V11() real ext-real non positive Element of REAL
Zeroseq is Element of the_set_of_RealSequences
l_add is non empty Relation-like [:the_set_of_RealSequences,the_set_of_RealSequences:] -defined the_set_of_RealSequences -valued Function-like V26([:the_set_of_RealSequences,the_set_of_RealSequences:]) V30([:the_set_of_RealSequences,the_set_of_RealSequences:], the_set_of_RealSequences ) Element of bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:]
l_mult is non empty Relation-like [:REAL,the_set_of_RealSequences:] -defined the_set_of_RealSequences -valued Function-like V26([:REAL,the_set_of_RealSequences:]) V30([:REAL,the_set_of_RealSequences:], the_set_of_RealSequences ) Element of bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:]
RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is non empty strict Abelian RLSStruct
the carrier of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is non empty set
l_norm is Relation-like the_set_of_l1RealSequences -defined REAL -valued Function-like V26( the_set_of_l1RealSequences ) V30( the_set_of_l1RealSequences , REAL ) V33() V34() V35() Element of bool [:the_set_of_l1RealSequences,REAL:]
l1_Space is non empty NORMSTR
Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences) is Element of the_set_of_l1RealSequences
Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences) is Relation-like [:the_set_of_l1RealSequences,the_set_of_l1RealSequences:] -defined the_set_of_l1RealSequences -valued Function-like V30([:the_set_of_l1RealSequences,the_set_of_l1RealSequences:], the_set_of_l1RealSequences ) Element of bool [:[:the_set_of_l1RealSequences,the_set_of_l1RealSequences:],the_set_of_l1RealSequences:]
[:the_set_of_l1RealSequences,the_set_of_l1RealSequences:] is set
[:[:the_set_of_l1RealSequences,the_set_of_l1RealSequences:],the_set_of_l1RealSequences:] is set
bool [:[:the_set_of_l1RealSequences,the_set_of_l1RealSequences:],the_set_of_l1RealSequences:] is non empty set
Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences) is Relation-like [:REAL,the_set_of_l1RealSequences:] -defined the_set_of_l1RealSequences -valued Function-like V30([:REAL,the_set_of_l1RealSequences:], the_set_of_l1RealSequences ) Element of bool [:[:REAL,the_set_of_l1RealSequences:],the_set_of_l1RealSequences:]
[:REAL,the_set_of_l1RealSequences:] is set
[:[:REAL,the_set_of_l1RealSequences:],the_set_of_l1RealSequences:] is set
bool [:[:REAL,the_set_of_l1RealSequences:],the_set_of_l1RealSequences:] is non empty set
NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #) is strict NORMSTR
the carrier of l1_Space is non empty set
0. l1_Space is V79( l1_Space ) Element of the carrier of l1_Space
the ZeroF of l1_Space is Element of the carrier of l1_Space
2 is 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
p is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . f is V11() real ext-real Element of REAL
p . f is V11() real ext-real Element of REAL
abs (p . f) is V11() real ext-real Element of REAL
(abs (p . f)) to_power lp is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq is set
lp . tseq is V11() real ext-real Element of REAL
f . tseq is V11() real ext-real Element of REAL
p . tseq is V11() real ext-real Element of REAL
abs (p . tseq) is V11() real ext-real Element of REAL
(abs (p . tseq)) to_power lp is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
lp is set
lp is set
bool the_set_of_RealSequences is non empty set
seq_id Zeroseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id Zeroseq),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . f is V11() real ext-real Element of REAL
(seq_id Zeroseq) . f is V11() real ext-real Element of REAL
abs ((seq_id Zeroseq) . f) is V11() real ext-real Element of REAL
(abs ((seq_id Zeroseq) . f)) to_power p is V11() real ext-real Element of REAL
abs 0 is V11() real ext-real V46() Element of REAL
(abs 0) to_power p is V11() real ext-real Element of REAL
0 to_power p is V11() real ext-real Element of REAL
lp is non empty Element of bool the carrier of Linear_Space_of_RealSequences
lp is non empty Element of bool the carrier of Linear_Space_of_RealSequences
f is set
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is set
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
p to_power lp is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
lp to_power p is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
lp * lp is V11() real ext-real Element of REAL
(lp * lp) to_power p is V11() real ext-real Element of REAL
lp to_power p is V11() real ext-real Element of REAL
(lp to_power p) * (lp to_power p) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
lp to_power lp is V11() real ext-real Element of REAL
p to_power lp is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
1 / p is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp + lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((lp + lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((lp + lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((lp + lp),p)) . f is V11() real ext-real Element of REAL
((Partial_Sums ((lp + lp),p)) . f) to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . f is V11() real ext-real Element of REAL
((Partial_Sums (lp,p)) . f) to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . f is V11() real ext-real Element of REAL
((Partial_Sums (lp,p)) . f) to_power (1 / p) is V11() real ext-real Element of REAL
(((Partial_Sums (lp,p)) . f) to_power (1 / p)) + (((Partial_Sums (lp,p)) . f) to_power (1 / p)) is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((lp + lp),p) . tseq is V11() real ext-real Element of REAL
(lp + lp) . tseq is V11() real ext-real Element of REAL
abs ((lp + lp) . tseq) is V11() real ext-real Element of REAL
(abs ((lp + lp) . tseq)) to_power p is V11() real ext-real Element of REAL
(lp,p) . tseq is V11() real ext-real Element of REAL
lp . tseq is V11() real ext-real Element of REAL
abs (lp . tseq) is V11() real ext-real Element of REAL
(abs (lp . tseq)) to_power p is V11() real ext-real Element of REAL
(lp,p) . tseq is V11() real ext-real Element of REAL
lp . tseq is V11() real ext-real Element of REAL
abs (lp . tseq) is V11() real ext-real Element of REAL
(abs (lp . tseq)) to_power p is V11() real ext-real Element of REAL
abs (lp + lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (abs (lp + lp)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums (abs (lp + lp))) . f is V11() real ext-real Element of REAL
abs lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (abs lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums (abs lp)) . f is V11() real ext-real Element of REAL
tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp + lp) . tv is V11() real ext-real Element of REAL
abs ((lp + lp) . tv) is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
abs (lp . tv) is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
abs (lp . tv) is V11() real ext-real Element of REAL
(abs (lp . tv)) + (abs (lp . tv)) is V11() real ext-real Element of REAL
(lp . tv) + (lp . tv) is V11() real ext-real Element of REAL
abs ((lp . tv) + (lp . tv)) is V11() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp + lp) . tv is V11() real ext-real Element of REAL
abs ((lp + lp) . tv) is V11() real ext-real Element of REAL
(abs (lp + lp)) . tv is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
abs (lp . tv) is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
abs (lp . tv) is V11() real ext-real Element of REAL
(abs (lp . tv)) + (abs (lp . tv)) is V11() real ext-real Element of REAL
tseq . tv is V11() real ext-real Element of REAL
Partial_Sums tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums tseq) . f is V11() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . tv is V11() real ext-real Element of REAL
abs (lp . tv) is V11() real ext-real Element of REAL
(abs lp) . tv is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
abs (lp . tv) is V11() real ext-real Element of REAL
abs lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(abs lp) . tv is V11() real ext-real Element of REAL
tseq . tv is V11() real ext-real Element of REAL
((abs lp) . tv) + ((abs lp) . tv) is V11() real ext-real Element of REAL
(abs lp) + (abs lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((abs lp) + (abs lp)) . tv is V11() real ext-real Element of REAL
tv is set
tseq . tv is V11() real ext-real Element of REAL
((abs lp) + (abs lp)) . tv is V11() real ext-real Element of REAL
Partial_Sums (abs lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums (abs lp)) . f is V11() real ext-real Element of REAL
Partial_Sums ((abs lp) + (abs lp)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums (abs lp)) + (Partial_Sums (abs lp)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p is V11() real ext-real Element of REAL
1 / p is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp + lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((lp + lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((lp + lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((lp + lp),p)) . e is V11() real ext-real Element of REAL
((Partial_Sums ((lp + lp),p)) . e) to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . e is V11() real ext-real Element of REAL
((Partial_Sums (lp,p)) . e) to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . e is V11() real ext-real Element of REAL
((Partial_Sums (lp,p)) . e) to_power (1 / p) is V11() real ext-real Element of REAL
(((Partial_Sums (lp,p)) . e) to_power (1 / p)) + (((Partial_Sums (lp,p)) . e) to_power (1 / p)) is V11() real ext-real Element of REAL
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp,p) . e1 is V11() real ext-real Element of REAL
lp . e1 is V11() real ext-real Element of REAL
abs (lp . e1) is V11() real ext-real Element of REAL
(abs (lp . e1)) to_power p is V11() real ext-real Element of REAL
(lp,p) . e1 is V11() real ext-real Element of REAL
lp . e1 is V11() real ext-real Element of REAL
abs (lp . e1) is V11() real ext-real Element of REAL
(abs (lp . e1)) to_power p is V11() real ext-real Element of REAL
((lp + lp),p) . e1 is V11() real ext-real Element of REAL
(lp + lp) . e1 is V11() real ext-real Element of REAL
abs ((lp + lp) . e1) is V11() real ext-real Element of REAL
(abs ((lp + lp) . e1)) to_power p is V11() real ext-real Element of REAL
(lp . e1) + (lp . e1) is V11() real ext-real Element of REAL
abs ((lp . e1) + (lp . e1)) is V11() real ext-real Element of REAL
(abs ((lp . e1) + (lp . e1))) to_power p is V11() real ext-real Element of REAL
p is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p + lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is V11() real ext-real Element of REAL
(p,lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((p + lp),lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((p + lp),lp) is V11() real ext-real Element of REAL
1 / lp is V11() real ext-real Element of REAL
(Sum ((p + lp),lp)) to_power (1 / lp) is V11() real ext-real Element of REAL
Sum (p,lp) is V11() real ext-real Element of REAL
(Sum (p,lp)) to_power (1 / lp) is V11() real ext-real Element of REAL
Sum (lp,lp) is V11() real ext-real Element of REAL
(Sum (lp,lp)) to_power (1 / lp) is V11() real ext-real Element of REAL
((Sum (p,lp)) to_power (1 / lp)) + ((Sum (lp,lp)) to_power (1 / lp)) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((p + lp),lp) . f is V11() real ext-real Element of REAL
(p + lp) . f is V11() real ext-real Element of REAL
abs ((p + lp) . f) is V11() real ext-real Element of REAL
(abs ((p + lp) . f)) to_power lp is V11() real ext-real Element of REAL
(p,lp) . f is V11() real ext-real Element of REAL
p . f is V11() real ext-real Element of REAL
abs (p . f) is V11() real ext-real Element of REAL
(abs (p . f)) to_power lp is V11() real ext-real Element of REAL
(lp,lp) . f is V11() real ext-real Element of REAL
lp . f is V11() real ext-real Element of REAL
abs (lp . f) is V11() real ext-real Element of REAL
(abs (lp . f)) to_power lp is V11() real ext-real Element of REAL
abs (p + lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id p is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs p is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(abs p) + (abs lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (abs lp) is V11() real ext-real Element of REAL
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq is Element of the carrier of l1_Space
||.tseq.|| is V11() real ext-real Element of REAL
the normF of l1_Space is non empty Relation-like the carrier of l1_Space -defined REAL -valued Function-like V26( the carrier of l1_Space) V30( the carrier of l1_Space, REAL ) V33() V34() V35() Element of bool [: the carrier of l1_Space,REAL:]
[: the carrier of l1_Space,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of l1_Space,REAL:] is non empty set
the normF of l1_Space . tseq is V11() real ext-real Element of REAL
the normF of l1_Space . tseq is V11() real ext-real Element of REAL
seq_id tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs (seq_id tseq) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (abs (seq_id tseq)) is V11() real ext-real Element of REAL
tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(abs (p + lp)) . e is V11() real ext-real Element of REAL
(p + lp) . e is V11() real ext-real Element of REAL
abs ((p + lp) . e) is V11() real ext-real Element of REAL
tv . e is V11() real ext-real Element of REAL
p . e is V11() real ext-real Element of REAL
abs (p . e) is V11() real ext-real Element of REAL
lp . e is V11() real ext-real Element of REAL
abs (lp . e) is V11() real ext-real Element of REAL
(abs (p . e)) + (abs (lp . e)) is V11() real ext-real Element of REAL
(abs p) . e is V11() real ext-real Element of REAL
((abs p) . e) + (abs (lp . e)) is V11() real ext-real Element of REAL
(abs lp) . e is V11() real ext-real Element of REAL
((abs p) . e) + ((abs lp) . e) is V11() real ext-real Element of REAL
(p . e) + (lp . e) is V11() real ext-real Element of REAL
abs ((p . e) + (lp . e)) is V11() real ext-real Element of REAL
f is Element of the carrier of l1_Space
||.f.|| is V11() real ext-real Element of REAL
the normF of l1_Space . f is V11() real ext-real Element of REAL
the normF of l1_Space . f is V11() real ext-real Element of REAL
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (abs (seq_id f)) is V11() real ext-real Element of REAL
f + tseq is Element of the carrier of l1_Space
the addF of l1_Space is non empty Relation-like [: the carrier of l1_Space, the carrier of l1_Space:] -defined the carrier of l1_Space -valued Function-like V26([: the carrier of l1_Space, the carrier of l1_Space:]) V30([: the carrier of l1_Space, the carrier of l1_Space:], the carrier of l1_Space) Element of bool [:[: the carrier of l1_Space, the carrier of l1_Space:], the carrier of l1_Space:]
[: the carrier of l1_Space, the carrier of l1_Space:] is non empty set
[:[: the carrier of l1_Space, the carrier of l1_Space:], the carrier of l1_Space:] is non empty set
bool [:[: the carrier of l1_Space, the carrier of l1_Space:], the carrier of l1_Space:] is non empty set
K473( the carrier of l1_Space, the addF of l1_Space,f,tseq) is Element of the carrier of l1_Space
[f,tseq] is set
{f,tseq} is non empty set
{f} is non empty set
{{f,tseq},{f}} is non empty set
the addF of l1_Space . [f,tseq] is set
||.(f + tseq).|| is V11() real ext-real Element of REAL
the normF of l1_Space . (f + tseq) is V11() real ext-real Element of REAL
the normF of l1_Space . (f + tseq) is V11() real ext-real Element of REAL
seq_id (f + tseq) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs (seq_id (f + tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (abs (seq_id (f + tseq))) is V11() real ext-real Element of REAL
(seq_id f) + (seq_id tseq) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id ((seq_id f) + (seq_id tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs (seq_id ((seq_id f) + (seq_id tseq))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (abs (seq_id ((seq_id f) + (seq_id tseq)))) is V11() real ext-real Element of REAL
abs ((seq_id f) + (seq_id tseq)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (abs ((seq_id f) + (seq_id tseq))) is V11() real ext-real Element of REAL
||.f.|| + ||.tseq.|| is V11() real ext-real Element of REAL
Sum (abs p) is V11() real ext-real Element of REAL
p is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p + lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is V11() real ext-real Element of REAL
(p,lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((p + lp),lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((p + lp),lp) is V11() real ext-real Element of REAL
1 / lp is V11() real ext-real Element of REAL
(Sum ((p + lp),lp)) to_power (1 / lp) is V11() real ext-real Element of REAL
Sum (p,lp) is V11() real ext-real Element of REAL
(Sum (p,lp)) to_power (1 / lp) is V11() real ext-real Element of REAL
Sum (lp,lp) is V11() real ext-real Element of REAL
(Sum (lp,lp)) to_power (1 / lp) is V11() real ext-real Element of REAL
((Sum (p,lp)) to_power (1 / lp)) + ((Sum (lp,lp)) to_power (1 / lp)) is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(p,lp) . e is V11() real ext-real Element of REAL
p . e is V11() real ext-real Element of REAL
abs (p . e) is V11() real ext-real Element of REAL
(abs (p . e)) to_power lp is V11() real ext-real Element of REAL
(lp,lp) . e is V11() real ext-real Element of REAL
lp . e is V11() real ext-real Element of REAL
abs (lp . e) is V11() real ext-real Element of REAL
(abs (lp . e)) to_power lp is V11() real ext-real Element of REAL
((p + lp),lp) . e is V11() real ext-real Element of REAL
(p + lp) . e is V11() real ext-real Element of REAL
abs ((p + lp) . e) is V11() real ext-real Element of REAL
(abs ((p + lp) . e)) to_power lp is V11() real ext-real Element of REAL
(p . e) + (lp . e) is V11() real ext-real Element of REAL
abs ((p . e) + (lp . e)) is V11() real ext-real Element of REAL
(abs ((p . e) + (lp . e))) to_power lp is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
lp is Element of the carrier of Linear_Space_of_RealSequences
f is Element of the carrier of Linear_Space_of_RealSequences
lp + f is Element of the carrier of Linear_Space_of_RealSequences
the addF of Linear_Space_of_RealSequences is non empty Relation-like [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) V30([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
K473( the carrier of Linear_Space_of_RealSequences, the addF of Linear_Space_of_RealSequences,lp,f) is Element of the carrier of Linear_Space_of_RealSequences
[lp,f] is set
{lp,f} is non empty set
{lp} is non empty set
{{lp,f},{lp}} is non empty set
the addF of Linear_Space_of_RealSequences . [lp,f] is set
seq_id (lp + f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (lp + f)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
1 / p is V11() real ext-real Element of REAL
tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(tseq,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id lp),p) . m is V11() real ext-real Element of REAL
(seq_id lp) . m is V11() real ext-real Element of REAL
abs ((seq_id lp) . m) is V11() real ext-real Element of REAL
(abs ((seq_id lp) . m)) to_power p is V11() real ext-real Element of REAL
((seq_id f),p) . m is V11() real ext-real Element of REAL
(seq_id f) . m is V11() real ext-real Element of REAL
abs ((seq_id f) . m) is V11() real ext-real Element of REAL
(abs ((seq_id f) . m)) to_power p is V11() real ext-real Element of REAL
Partial_Sums ((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
dom (Partial_Sums ((seq_id lp),p)) is V52() V53() V54() V55() V56() V57() set
m is V11() real ext-real set
i is set
((seq_id lp),p) . 0 is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id lp),p)) . 0 is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((seq_id lp),p)) . i is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id lp),p)) . i is V11() real ext-real Element of REAL
((Partial_Sums ((seq_id lp),p)) . i) to_power (1 / p) is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id lp) + (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id ((seq_id lp) + (seq_id f)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
dom (Partial_Sums ((seq_id f),p)) is V52() V53() V54() V55() V56() V57() set
m is V11() real ext-real set
c is set
((seq_id f),p) . 0 is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id f),p)) . 0 is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((seq_id f),p)) . g is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
b to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id f),p)) . c is V11() real ext-real Element of REAL
((Partial_Sums ((seq_id f),p)) . c) to_power (1 / p) is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
(i,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
i + c is V11() real ext-real Element of REAL
p * (1 / p) is V11() real ext-real Element of REAL
p * 1 is V11() real ext-real Element of REAL
(p * 1) / p is V11() real ext-real Element of REAL
tseq + i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((tseq + i),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((tseq + i),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((tseq + i),p)) . n is V11() real ext-real Element of REAL
((Partial_Sums ((tseq + i),p)) . n) to_power (1 / p) is V11() real ext-real Element of REAL
(((Partial_Sums ((tseq + i),p)) . n) to_power (1 / p)) to_power p is V11() real ext-real Element of REAL
(1 / p) * p is V11() real ext-real Element of REAL
((Partial_Sums ((tseq + i),p)) . n) to_power ((1 / p) * p) is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id f),p)) . n is V11() real ext-real Element of REAL
((Partial_Sums ((seq_id f),p)) . n) to_power (1 / p) is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id lp),p)) . n is V11() real ext-real Element of REAL
((Partial_Sums ((seq_id lp),p)) . n) to_power (1 / p) is V11() real ext-real Element of REAL
(((Partial_Sums ((seq_id f),p)) . n) to_power (1 / p)) + (((Partial_Sums ((seq_id lp),p)) . n) to_power (1 / p)) is V11() real ext-real Element of REAL
0 to_power p is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(tseq + i) . n is V11() real ext-real Element of REAL
abs ((tseq + i) . n) is V11() real ext-real Element of REAL
((tseq + i),p) . n is V11() real ext-real Element of REAL
(abs ((tseq + i) . n)) to_power p is V11() real ext-real Element of REAL
((tseq + i),p) . 0 is V11() real ext-real Element of REAL
(Partial_Sums ((tseq + i),p)) . 0 is V11() real ext-real Element of REAL
(i + c) to_power p is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((tseq + i),p) . n is V11() real ext-real Element of REAL
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id lp) + (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id ((seq_id lp) + (seq_id f)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is set
lp is V11() real ext-real Element of REAL
f is Element of the carrier of Linear_Space_of_RealSequences
lp * f is Element of the carrier of Linear_Space_of_RealSequences
the Mult of Linear_Space_of_RealSequences is non empty Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([:REAL, the carrier of Linear_Space_of_RealSequences:]) V30([:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[:REAL, the carrier of Linear_Space_of_RealSequences:] is non empty set
[:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
K469( the Mult of Linear_Space_of_RealSequences,lp,f) is set
[lp,f] is set
{lp,f} is non empty set
{lp} is non empty V52() V53() V54() set
{{lp,f},{lp}} is non empty set
the Mult of Linear_Space_of_RealSequences . [lp,f] is set
seq_id (lp * f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (lp * f)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(seq_id f) . tv is V11() real ext-real Element of REAL
abs ((seq_id f) . tv) is V11() real ext-real Element of REAL
((seq_id f),p) . tv is V11() real ext-real Element of REAL
(abs ((seq_id f) . tv)) to_power p is V11() real ext-real Element of REAL
Partial_Sums ((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
dom (Partial_Sums ((seq_id f),p)) is V52() V53() V54() V55() V56() V57() set
tv is V11() real ext-real set
lp (#) (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id (lp (#) (seq_id f)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id (lp * f)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs lp is V11() real ext-real Element of REAL
(abs lp) to_power p is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((seq_id (lp * f)),p)) . e is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id f),p)) . e is V11() real ext-real Element of REAL
((abs lp) to_power p) * ((Partial_Sums ((seq_id f),p)) . e) is V11() real ext-real Element of REAL
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(seq_id f) . e1 is V11() real ext-real Element of REAL
abs ((seq_id f) . e1) is V11() real ext-real Element of REAL
(lp (#) (seq_id f)) . e1 is V11() real ext-real Element of REAL
lp * ((seq_id f) . e1) is V11() real ext-real Element of REAL
((lp (#) (seq_id f)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((lp (#) (seq_id f)),p) . e1 is V11() real ext-real Element of REAL
abs ((lp (#) (seq_id f)) . e1) is V11() real ext-real Element of REAL
(abs ((lp (#) (seq_id f)) . e1)) to_power p is V11() real ext-real Element of REAL
(abs lp) * (abs ((seq_id f) . e1)) is V11() real ext-real Element of REAL
((abs lp) * (abs ((seq_id f) . e1))) to_power p is V11() real ext-real Element of REAL
(abs ((seq_id f) . e1)) to_power p is V11() real ext-real Element of REAL
((abs lp) to_power p) * ((abs ((seq_id f) . e1)) to_power p) is V11() real ext-real Element of REAL
((seq_id (lp * f)),p) . e1 is V11() real ext-real Element of REAL
((seq_id f),p) . e1 is V11() real ext-real Element of REAL
((abs lp) to_power p) * (((seq_id f),p) . e1) is V11() real ext-real Element of REAL
((abs lp) to_power p) (#) ((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(((abs lp) to_power p) (#) ((seq_id f),p)) . e1 is V11() real ext-real Element of REAL
e1 is set
((seq_id (lp * f)),p) . e1 is V11() real ext-real Element of REAL
(((abs lp) to_power p) (#) ((seq_id f),p)) . e1 is V11() real ext-real Element of REAL
Partial_Sums (((abs lp) to_power p) (#) ((seq_id f),p)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((abs lp) to_power p) (#) (Partial_Sums ((seq_id f),p)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is set
dom (Partial_Sums ((seq_id (lp * f)),p)) is V52() V53() V54() V55() V56() V57() set
((abs lp) to_power p) * tv is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id f),p)) . e is V11() real ext-real Element of REAL
((abs lp) to_power p) * ((Partial_Sums ((seq_id f),p)) . e) is V11() real ext-real Element of REAL
e is set
(Partial_Sums ((seq_id (lp * f)),p)) . e is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id f),p)) . e is V11() real ext-real Element of REAL
((abs lp) to_power p) * ((Partial_Sums ((seq_id f),p)) . e) is V11() real ext-real Element of REAL
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums ((seq_id (lp * f)),p)) . e1 is V11() real ext-real Element of REAL
(((abs lp) to_power p) * tv) + 1 is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
e1 is V11() real ext-real set
m is set
(Partial_Sums ((seq_id (lp * f)),p)) . m is V11() real ext-real Element of REAL
m is set
(Partial_Sums ((seq_id (lp * f)),p)) . m is V11() real ext-real Element of REAL
e is V11() real ext-real set
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id (lp * f)),p) . e1 is V11() real ext-real Element of REAL
(lp (#) (seq_id f)) . e1 is V11() real ext-real Element of REAL
(seq_id f) . e1 is V11() real ext-real Element of REAL
lp * ((seq_id f) . e1) is V11() real ext-real Element of REAL
((lp (#) (seq_id f)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((lp (#) (seq_id f)),p) . e1 is V11() real ext-real Element of REAL
abs (lp * ((seq_id f) . e1)) is V11() real ext-real Element of REAL
(abs (lp * ((seq_id f) . e1))) to_power p is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
RLSStruct(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)) #) is non empty strict RLSStruct
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
RLSStruct(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)) #) is non empty strict RLSStruct
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
RLSStruct(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)) #) is non empty strict RLSStruct
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
1 / p is V11() real ext-real Element of REAL
lp is set
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id lp),p) is V11() real ext-real Element of REAL
(Sum ((seq_id lp),p)) to_power (1 / p) is V11() real ext-real Element of REAL
lp is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
lp is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
lp is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
f is set
lp . f is V11() real ext-real Element of REAL
lp . f is V11() real ext-real Element of REAL
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id f),p) is V11() real ext-real Element of REAL
(Sum ((seq_id f),p)) to_power (1 / p) is V11() real ext-real Element of REAL
dom lp is set
dom lp is set
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
RLSStruct(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)) #) is non empty strict RLSStruct
lp is V11() real ext-real Element of REAL
(lp) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((lp),Linear_Space_of_RealSequences) is Element of (lp)
Add_ ((lp),Linear_Space_of_RealSequences) is non empty Relation-like [:(lp),(lp):] -defined (lp) -valued Function-like V26([:(lp),(lp):]) V30([:(lp),(lp):],(lp)) Element of bool [:[:(lp),(lp):],(lp):]
[:(lp),(lp):] is non empty set
[:[:(lp),(lp):],(lp):] is non empty set
bool [:[:(lp),(lp):],(lp):] is non empty set
Mult_ ((lp),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(lp):] -defined (lp) -valued Function-like V26([:REAL,(lp):]) V30([:REAL,(lp):],(lp)) Element of bool [:[:REAL,(lp):],(lp):]
[:REAL,(lp):] is non empty set
[:[:REAL,(lp):],(lp):] is non empty set
bool [:[:REAL,(lp):],(lp):] is non empty set
(lp) is non empty Relation-like (lp) -defined REAL -valued Function-like V26((lp)) V30((lp), REAL ) V33() V34() V35() Element of bool [:(lp),REAL:]
[:(lp),REAL:] is non empty V33() V34() V35() set
bool [:(lp),REAL:] is non empty set
NORMSTR(# (lp),(Zero_ ((lp),Linear_Space_of_RealSequences)),(Add_ ((lp),Linear_Space_of_RealSequences)),(Mult_ ((lp),Linear_Space_of_RealSequences)),(lp) #) is strict NORMSTR
f is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of f is non empty set
the ZeroF of f is Element of the carrier of f
the addF of f is non empty Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like V26([: the carrier of f, the carrier of f:]) V30([: the carrier of f, the carrier of f:], the carrier of f) Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the Mult of f is non empty Relation-like [:REAL, the carrier of f:] -defined the carrier of f -valued Function-like V26([:REAL, the carrier of f:]) V30([:REAL, the carrier of f:], the carrier of f) Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:REAL, the carrier of f:] is non empty set
[:[:REAL, the carrier of f:], the carrier of f:] is non empty set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty set
RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #) is non empty strict RLSStruct
[:REAL, the carrier of Linear_Space_of_RealSequences:] is non empty set
the Mult of Linear_Space_of_RealSequences is non empty Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([:REAL, the carrier of Linear_Space_of_RealSequences:]) V30([:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
the Mult of Linear_Space_of_RealSequences | [:REAL, the carrier of f:] is Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
0. RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #) is V79( RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #)) Element of the carrier of RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #)
the carrier of RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #) is non empty set
the ZeroF of RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #) is Element of the carrier of RLSStruct(# the carrier of f, the ZeroF of f, the addF of f, the Mult of f #)
0. Linear_Space_of_RealSequences is V79( Linear_Space_of_RealSequences ) Element of the carrier of Linear_Space_of_RealSequences
the ZeroF of Linear_Space_of_RealSequences is Element of the carrier of Linear_Space_of_RealSequences
0. f is V79(f) Element of the carrier of f
the addF of Linear_Space_of_RealSequences is non empty Relation-like [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) V30([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
the addF of Linear_Space_of_RealSequences || the carrier of f is Relation-like Function-like set
the addF of Linear_Space_of_RealSequences | [: the carrier of f, the carrier of f:] is Relation-like set
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
1 / p is V11() real ext-real Element of REAL
lp is non empty NORMSTR
the carrier of lp is non empty set
0. lp is V79(lp) Element of the carrier of lp
the ZeroF of lp is Element of the carrier of lp
lp is Element of the carrier of lp
||.lp.|| is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . lp is V11() real ext-real Element of REAL
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id lp),p) is V11() real ext-real Element of REAL
(Sum ((seq_id lp),p)) to_power (1 / p) is V11() real ext-real Element of REAL
lp is Element of the carrier of lp
f is Element of the carrier of lp
lp + f is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,lp,f) is Element of the carrier of lp
[lp,f] is set
{lp,f} is non empty set
{lp} is non empty set
{{lp,f},{lp}} is non empty set
the addF of lp . [lp,f] is set
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id lp) + (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
the addF of Linear_Space_of_RealSequences is non empty Relation-like [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) V30([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
dom the addF of Linear_Space_of_RealSequences is Relation-like set
the addF of Linear_Space_of_RealSequences || (p) is Relation-like Function-like set
the addF of Linear_Space_of_RealSequences | [:(p),(p):] is Relation-like set
dom ( the addF of Linear_Space_of_RealSequences || (p)) is set
[:(p),(p):] is non empty Relation-like the carrier of Linear_Space_of_RealSequences -defined the carrier of Linear_Space_of_RealSequences -valued Element of bool [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]
bool [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty set
[lp,f] is Element of [: the carrier of lp, the carrier of lp:]
( the addF of Linear_Space_of_RealSequences || (p)) . [lp,f] is set
tseq is Element of the carrier of Linear_Space_of_RealSequences
tv is Element of the carrier of Linear_Space_of_RealSequences
tseq + tv is Element of the carrier of Linear_Space_of_RealSequences
K473( the carrier of Linear_Space_of_RealSequences, the addF of Linear_Space_of_RealSequences,tseq,tv) is Element of the carrier of Linear_Space_of_RealSequences
[tseq,tv] is set
{tseq,tv} is non empty set
{tseq} is non empty set
{{tseq,tv},{tseq}} is non empty set
the addF of Linear_Space_of_RealSequences . [tseq,tv] is set
tseq is V11() real ext-real Element of REAL
tv is Element of the carrier of lp
tseq * tv is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,tseq,tv) is set
[tseq,tv] is set
{tseq,tv} is non empty set
{tseq} is non empty V52() V53() V54() set
{{tseq,tv},{tseq}} is non empty set
the Mult of lp . [tseq,tv] is set
seq_id tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq (#) (seq_id tv) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
the Mult of Linear_Space_of_RealSequences is non empty Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([:REAL, the carrier of Linear_Space_of_RealSequences:]) V30([:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[:REAL, the carrier of Linear_Space_of_RealSequences:] is non empty set
[:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
dom the Mult of Linear_Space_of_RealSequences is Relation-like set
the Mult of Linear_Space_of_RealSequences | [:REAL,(p):] is Relation-like [:REAL, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like Element of bool [:[:REAL, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,(p):]) is Relation-like set
[tseq,tv] is Element of [:REAL, the carrier of lp:]
( the Mult of Linear_Space_of_RealSequences | [:REAL,(p):]) . [tseq,tv] is set
e is Element of the carrier of Linear_Space_of_RealSequences
tseq * e is Element of the carrier of Linear_Space_of_RealSequences
K469( the Mult of Linear_Space_of_RealSequences,tseq,e) is set
[tseq,e] is set
{tseq,e} is non empty set
{{tseq,e},{tseq}} is non empty set
the Mult of Linear_Space_of_RealSequences . [tseq,e] is set
0. Linear_Space_of_RealSequences is V79( Linear_Space_of_RealSequences ) Element of the carrier of Linear_Space_of_RealSequences
the ZeroF of Linear_Space_of_RealSequences is Element of the carrier of Linear_Space_of_RealSequences
lp is set
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is set
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is Element of the carrier of lp
- lp is Element of the carrier of lp
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id lp) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
seq_id (- lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(- 1) * lp is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,(- 1),lp) is set
[(- 1),lp] is set
{(- 1),lp} is non empty set
{(- 1)} is non empty V52() V53() V54() set
{{(- 1),lp},{(- 1)}} is non empty set
the Mult of lp . [(- 1),lp] is set
lp is Element of the carrier of lp
f is Element of the carrier of lp
lp - f is Element of the carrier of lp
- f is Element of the carrier of lp
lp + (- f) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,lp,(- f)) is Element of the carrier of lp
[lp,(- f)] is set
{lp,(- f)} is non empty set
{lp} is non empty set
{{lp,(- f)},{lp}} is non empty set
the addF of lp . [lp,(- f)] is set
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id lp) - (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id f) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id f) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id lp) + (- (seq_id f)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
seq_id (- f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id lp) + (seq_id (- f)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is set
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is set
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq is Element of the carrier of lp
seq_id tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is Element of the carrier of lp
e is Element of the carrier of lp
tv + e is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,tv,e) is Element of the carrier of lp
[tv,e] is set
{tv,e} is non empty set
{tv} is non empty set
{{tv,e},{tv}} is non empty set
the addF of lp . [tv,e] is set
seq_id tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id e is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tv) + (seq_id e) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
m is Element of the carrier of lp
e1 is V11() real ext-real Element of REAL
e1 * m is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,e1,m) is set
[e1,m] is set
{e1,m} is non empty set
{e1} is non empty V52() V53() V54() set
{{e1,m},{e1}} is non empty set
the Mult of lp . [e1,m] is set
seq_id m is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e1 (#) (seq_id m) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
n is Element of the carrier of lp
- n is Element of the carrier of lp
seq_id n is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id n) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id n) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
i is Element of the carrier of lp
- i is Element of the carrier of lp
seq_id (- i) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id i) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
K38(1) (#) (seq_id i) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
i is Element of the carrier of lp
m is Element of the carrier of lp
i - m is Element of the carrier of lp
- m is Element of the carrier of lp
i + (- m) is Element of the carrier of lp
K473( the carrier of lp, the addF of lp,i,(- m)) is Element of the carrier of lp
[i,(- m)] is set
{i,(- m)} is non empty set
{i} is non empty set
{{i,(- m)},{i}} is non empty set
the addF of lp . [i,(- m)] is set
seq_id i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id m is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id i) - (seq_id m) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id m) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) (#) (seq_id m) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id i) + (- (seq_id m)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
b is Element of the carrier of lp
seq_id b is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id b),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
c is Element of the carrier of lp
||.c.|| is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . c is V11() real ext-real Element of REAL
seq_id c is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id c),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id c),p) is V11() real ext-real Element of REAL
(Sum ((seq_id c),p)) to_power (1 / p) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
1 / p is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (lp,p) is V11() real ext-real Element of REAL
(Sum (lp,p)) to_power (1 / p) is V11() real ext-real Element of REAL
lp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp,p) . lp is V11() real ext-real Element of REAL
lp . lp is V11() real ext-real Element of REAL
abs (lp . lp) is V11() real ext-real Element of REAL
(abs (lp . lp)) to_power p is V11() real ext-real Element of REAL
Partial_Sums (lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (lp,p)) . lp is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp,p) . f is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . f is V11() real ext-real Element of REAL
f + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp,p) . (f + 1) is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . (f + 1) is V11() real ext-real Element of REAL
0 + ((lp,p) . (f + 1)) is V11() real ext-real Element of REAL
((lp,p) . f) + ((lp,p) . (f + 1)) is V11() real ext-real Element of REAL
(lp,p) . 0 is V11() real ext-real Element of REAL
(Partial_Sums (lp,p)) . 0 is V11() real ext-real Element of REAL
(lp,p) . lp is V11() real ext-real Element of REAL
lp is V11() real ext-real set
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (lp,p)) . f is V11() real ext-real Element of REAL
((Partial_Sums (lp,p)) . f) - 0 is V11() real ext-real Element of REAL
abs (((Partial_Sums (lp,p)) . f) - 0) is V11() real ext-real Element of REAL
0 - 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V52() V53() V54() V55() V56() V57() V58() Element of REAL
abs (0 - 0) is V11() real ext-real Element of REAL
lim (Partial_Sums (lp,p)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
1 / p is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (lp,p) is V11() real ext-real Element of REAL
(Sum (lp,p)) to_power (1 / p) is V11() real ext-real Element of REAL
lp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp,p) . lp is V11() real ext-real Element of REAL
lp . lp is V11() real ext-real Element of REAL
abs (lp . lp) is V11() real ext-real Element of REAL
(abs (lp . lp)) to_power p is V11() real ext-real Element of REAL
((Sum (lp,p)) to_power (1 / p)) to_power p is V11() real ext-real Element of REAL
(1 / p) * p is V11() real ext-real Element of REAL
(Sum (lp,p)) to_power ((1 / p) * p) is V11() real ext-real Element of REAL
(Sum (lp,p)) to_power 1 is V11() real ext-real Element of REAL
lp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
0 to_power (1 / p) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(lp,p) . f is V11() real ext-real Element of REAL
lp . f is V11() real ext-real Element of REAL
abs (lp . f) is V11() real ext-real Element of REAL
(abs (lp . f)) to_power p is V11() real ext-real Element of REAL
lp . lp is V11() real ext-real Element of REAL
abs (lp . lp) is V11() real ext-real Element of REAL
(abs (lp . lp)) to_power p is V11() real ext-real Element of REAL
((abs (lp . lp)) to_power p) to_power (1 / p) is V11() real ext-real Element of REAL
p * (1 / p) is V11() real ext-real Element of REAL
(abs (lp . lp)) to_power (p * (1 / p)) is V11() real ext-real Element of REAL
(abs (lp . lp)) to_power 1 is V11() real ext-real Element of REAL
lp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real set
lp . lp is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
lp is non empty NORMSTR
the carrier of lp is non empty set
lp is Element of the carrier of lp
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is V11() real ext-real Element of REAL
f * lp is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,f,lp) is set
[f,lp] is set
{f,lp} is non empty set
{f} is non empty V52() V53() V54() set
{{f,lp},{f}} is non empty set
the Mult of lp . [f,lp] is set
seq_id (f * lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (f * lp)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
abs f is V11() real ext-real Element of REAL
(abs f) to_power p is V11() real ext-real Element of REAL
((abs f) to_power p) (#) ((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq is set
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(seq_id lp) . tv is V11() real ext-real Element of REAL
abs ((seq_id lp) . tv) is V11() real ext-real Element of REAL
((seq_id (f * lp)),p) . tv is V11() real ext-real Element of REAL
(seq_id (f * lp)) . tv is V11() real ext-real Element of REAL
abs ((seq_id (f * lp)) . tv) is V11() real ext-real Element of REAL
(abs ((seq_id (f * lp)) . tv)) to_power p is V11() real ext-real Element of REAL
f (#) (seq_id lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id (f (#) (seq_id lp)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (f (#) (seq_id lp))) . tv is V11() real ext-real Element of REAL
abs ((seq_id (f (#) (seq_id lp))) . tv) is V11() real ext-real Element of REAL
(abs ((seq_id (f (#) (seq_id lp))) . tv)) to_power p is V11() real ext-real Element of REAL
(f (#) (seq_id lp)) . tv is V11() real ext-real Element of REAL
abs ((f (#) (seq_id lp)) . tv) is V11() real ext-real Element of REAL
(abs ((f (#) (seq_id lp)) . tv)) to_power p is V11() real ext-real Element of REAL
f * ((seq_id lp) . tv) is V11() real ext-real Element of REAL
abs (f * ((seq_id lp) . tv)) is V11() real ext-real Element of REAL
(abs (f * ((seq_id lp) . tv))) to_power p is V11() real ext-real Element of REAL
(abs f) * (abs ((seq_id lp) . tv)) is V11() real ext-real Element of REAL
((abs f) * (abs ((seq_id lp) . tv))) to_power p is V11() real ext-real Element of REAL
(abs ((seq_id lp) . tv)) to_power p is V11() real ext-real Element of REAL
((abs f) to_power p) * ((abs ((seq_id lp) . tv)) to_power p) is V11() real ext-real Element of REAL
((seq_id lp),p) . tv is V11() real ext-real Element of REAL
((abs f) to_power p) * (((seq_id lp),p) . tv) is V11() real ext-real Element of REAL
(((abs f) to_power p) (#) ((seq_id lp),p)) . tv is V11() real ext-real Element of REAL
((seq_id (f * lp)),p) . tseq is V11() real ext-real Element of REAL
(((abs f) to_power p) (#) ((seq_id lp),p)) . tseq is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
lp is non empty NORMSTR
the carrier of lp is non empty set
lp is Element of the carrier of lp
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id lp),p) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f * lp is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,f,lp) is set
[f,lp] is set
{f,lp} is non empty set
{f} is non empty V52() V53() V54() set
{{f,lp},{f}} is non empty set
the Mult of lp . [f,lp] is set
seq_id (f * lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (f * lp)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id (f * lp)),p) is V11() real ext-real Element of REAL
abs f is V11() real ext-real Element of REAL
(abs f) to_power p is V11() real ext-real Element of REAL
((abs f) to_power p) * (Sum ((seq_id lp),p)) is V11() real ext-real Element of REAL
((abs f) to_power p) (#) ((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (((abs f) to_power p) (#) ((seq_id lp),p)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
1 / p is V11() real ext-real Element of REAL
lp is non empty NORMSTR
the carrier of lp is non empty set
lp is Element of the carrier of lp
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id lp),p) is V11() real ext-real Element of REAL
(Sum ((seq_id lp),p)) to_power (1 / p) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id lp),p) . f is V11() real ext-real Element of REAL
(seq_id lp) . f is V11() real ext-real Element of REAL
abs ((seq_id lp) . f) is V11() real ext-real Element of REAL
(abs ((seq_id lp) . f)) to_power p is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f * lp is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,f,lp) is set
[f,lp] is set
{f,lp} is non empty set
{f} is non empty V52() V53() V54() set
{{f,lp},{f}} is non empty set
the Mult of lp . [f,lp] is set
seq_id (f * lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (f * lp)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id (f * lp)),p) is V11() real ext-real Element of REAL
(Sum ((seq_id (f * lp)),p)) to_power (1 / p) is V11() real ext-real Element of REAL
abs f is V11() real ext-real Element of REAL
(abs f) * ((Sum ((seq_id lp),p)) to_power (1 / p)) is V11() real ext-real Element of REAL
(abs f) to_power p is V11() real ext-real Element of REAL
((abs f) to_power p) * (Sum ((seq_id lp),p)) is V11() real ext-real Element of REAL
(((abs f) to_power p) * (Sum ((seq_id lp),p))) to_power (1 / p) is V11() real ext-real Element of REAL
((abs f) to_power p) to_power (1 / p) is V11() real ext-real Element of REAL
(((abs f) to_power p) to_power (1 / p)) * ((Sum ((seq_id lp),p)) to_power (1 / p)) is V11() real ext-real Element of REAL
p * (1 / p) is V11() real ext-real Element of REAL
(abs f) to_power (p * (1 / p)) is V11() real ext-real Element of REAL
((abs f) to_power (p * (1 / p))) * ((Sum ((seq_id lp),p)) to_power (1 / p)) is V11() real ext-real Element of REAL
(abs f) to_power 1 is V11() real ext-real Element of REAL
((abs f) to_power 1) * ((Sum ((seq_id lp),p)) to_power (1 / p)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
1 / p is V11() real ext-real Element of REAL
lp is non empty NORMSTR
the carrier of lp is non empty set
0. lp is V79(lp) Element of the carrier of lp
the ZeroF of lp is Element of the carrier of lp
lp is Element of the carrier of lp
||.lp.|| is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . lp is V11() real ext-real Element of REAL
f is Element of the carrier of lp
lp + f is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,lp,f) is Element of the carrier of lp
[lp,f] is set
{lp,f} is non empty set
{lp} is non empty set
{{lp,f},{lp}} is non empty set
the addF of lp . [lp,f] is set
||.(lp + f).|| is V11() real ext-real Element of REAL
the normF of lp . (lp + f) is V11() real ext-real Element of REAL
||.f.|| is V11() real ext-real Element of REAL
the normF of lp . f is V11() real ext-real Element of REAL
||.lp.|| + ||.f.|| is V11() real ext-real Element of REAL
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id f),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
the normF of lp . f is V11() real ext-real Element of REAL
Sum ((seq_id f),p) is V11() real ext-real Element of REAL
(Sum ((seq_id f),p)) to_power (1 / p) is V11() real ext-real Element of REAL
the normF of lp . lp is V11() real ext-real Element of REAL
seq_id lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id lp),p) is V11() real ext-real Element of REAL
(Sum ((seq_id lp),p)) to_power (1 / p) is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(seq_id lp) . tseq is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(seq_id lp) . tseq is V11() real ext-real Element of REAL
tseq is V11() real ext-real Element of REAL
tseq * lp is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,tseq,lp) is set
[tseq,lp] is set
{tseq,lp} is non empty set
{tseq} is non empty V52() V53() V54() set
{{tseq,lp},{tseq}} is non empty set
the Mult of lp . [tseq,lp] is set
||.(tseq * lp).|| is V11() real ext-real Element of REAL
the normF of lp . (tseq * lp) is V11() real ext-real Element of REAL
abs tseq is V11() real ext-real Element of REAL
(abs tseq) * ||.lp.|| is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id lp),p) . e is V11() real ext-real Element of REAL
(seq_id lp) . e is V11() real ext-real Element of REAL
abs ((seq_id lp) . e) is V11() real ext-real Element of REAL
(abs ((seq_id lp) . e)) to_power p is V11() real ext-real Element of REAL
(seq_id lp) + (seq_id f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id ((seq_id lp) + (seq_id f)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id (lp + f) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(((seq_id lp) + (seq_id f)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (((seq_id lp) + (seq_id f)),p) is V11() real ext-real Element of REAL
(Sum (((seq_id lp) + (seq_id f)),p)) to_power (1 / p) is V11() real ext-real Element of REAL
the normF of lp . (lp + f) is V11() real ext-real Element of REAL
the normF of lp . (tseq * lp) is V11() real ext-real Element of REAL
seq_id (tseq * lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (tseq * lp)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id (tseq * lp)),p) is V11() real ext-real Element of REAL
(Sum ((seq_id (tseq * lp)),p)) to_power (1 / p) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
lp is non empty NORMSTR
0. lp is V79(lp) Element of the carrier of lp
the carrier of lp is non empty set
the ZeroF of lp is Element of the carrier of lp
||.(0. lp).|| is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . (0. lp) is V11() real ext-real Element of REAL
lp is Element of the carrier of lp
||.lp.|| is V11() real ext-real Element of REAL
the normF of lp . lp is V11() real ext-real Element of REAL
f is Element of the carrier of lp
||.f.|| is V11() real ext-real Element of REAL
the normF of lp . f is V11() real ext-real Element of REAL
tseq is Element of the carrier of lp
||.tseq.|| is V11() real ext-real Element of REAL
the normF of lp . tseq is V11() real ext-real Element of REAL
tv is Element of the carrier of lp
e is Element of the carrier of lp
tv + e is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,tv,e) is Element of the carrier of lp
[tv,e] is set
{tv,e} is non empty set
{tv} is non empty set
{{tv,e},{tv}} is non empty set
the addF of lp . [tv,e] is set
||.(tv + e).|| is V11() real ext-real Element of REAL
the normF of lp . (tv + e) is V11() real ext-real Element of REAL
||.tv.|| is V11() real ext-real Element of REAL
the normF of lp . tv is V11() real ext-real Element of REAL
||.e.|| is V11() real ext-real Element of REAL
the normF of lp . e is V11() real ext-real Element of REAL
||.tv.|| + ||.e.|| is V11() real ext-real Element of REAL
e1 is Element of the carrier of lp
m is V11() real ext-real Element of REAL
m * e1 is Element of the carrier of lp
the Mult of lp is non empty Relation-like [:REAL, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([:REAL, the carrier of lp:]) V30([:REAL, the carrier of lp:], the carrier of lp) Element of bool [:[:REAL, the carrier of lp:], the carrier of lp:]
[:REAL, the carrier of lp:] is non empty set
[:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[:REAL, the carrier of lp:], the carrier of lp:] is non empty set
K469( the Mult of lp,m,e1) is set
[m,e1] is set
{m,e1} is non empty set
{m} is non empty V52() V53() V54() set
{{m,e1},{m}} is non empty set
the Mult of lp . [m,e1] is set
||.(m * e1).|| is V11() real ext-real Element of REAL
the normF of lp . (m * e1) is V11() real ext-real Element of REAL
abs m is V11() real ext-real Element of REAL
||.e1.|| is V11() real ext-real Element of REAL
the normF of lp . e1 is V11() real ext-real Element of REAL
(abs m) * ||.e1.|| is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
lp is non empty NORMSTR
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
p is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim lp is V11() real ext-real Element of REAL
(lim lp) - lp is V11() real ext-real Element of REAL
abs ((lim lp) - lp) is V11() real ext-real Element of REAL
(abs ((lim lp) - lp)) to_power p is V11() real ext-real Element of REAL
f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim tseq is V11() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
tseq . tv is V11() real ext-real Element of REAL
f . tv is V11() real ext-real Element of REAL
(f . tv) to_power p is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
(lp . tv) - lp is V11() real ext-real Element of REAL
abs ((lp . tv) - lp) is V11() real ext-real Element of REAL
(abs ((lp . tv) - lp)) to_power p is V11() real ext-real Element of REAL
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
f . tv is V11() real ext-real Element of REAL
lp . tv is V11() real ext-real Element of REAL
(lp . tv) - lp is V11() real ext-real Element of REAL
abs ((lp . tv) - lp) is V11() real ext-real Element of REAL
lim f is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
lp is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim lp is V11() real ext-real Element of REAL
(lim lp) - lp is V11() real ext-real Element of REAL
abs ((lim lp) - lp) is V11() real ext-real Element of REAL
(abs ((lim lp) - lp)) to_power p is V11() real ext-real Element of REAL
lim f is V11() real ext-real Element of REAL
((abs ((lim lp) - lp)) to_power p) + (lim f) is V11() real ext-real Element of REAL
tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim tv is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
tv . e is V11() real ext-real Element of REAL
lp . e is V11() real ext-real Element of REAL
(lp . e) - lp is V11() real ext-real Element of REAL
abs ((lp . e) - lp) is V11() real ext-real Element of REAL
(abs ((lp . e) - lp)) to_power p is V11() real ext-real Element of REAL
f . e is V11() real ext-real Element of REAL
((abs ((lp . e) - lp)) to_power p) + (f . e) is V11() real ext-real Element of REAL
tseq . e is V11() real ext-real Element of REAL
(tseq . e) + (f . e) is V11() real ext-real Element of REAL
tseq + f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim tseq is V11() real ext-real Element of REAL
p is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p + lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(p + lp) - lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- lp is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) lp is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(p + lp) + (- lp) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
- lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp + (- lp) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p + (lp + (- lp)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(p + (lp + (- lp))) . lp is V11() real ext-real Element of REAL
p . lp is V11() real ext-real Element of REAL
(lp + (- lp)) . lp is V11() real ext-real Element of REAL
(p . lp) + ((lp + (- lp)) . lp) is V11() real ext-real Element of REAL
lp . lp is V11() real ext-real Element of REAL
(- lp) . lp is V11() real ext-real Element of REAL
(lp . lp) + ((- lp) . lp) is V11() real ext-real Element of REAL
(p . lp) + ((lp . lp) + ((- lp) . lp)) is V11() real ext-real Element of REAL
- (lp . lp) is V11() real ext-real Element of REAL
(lp . lp) + (- (lp . lp)) is V11() real ext-real Element of REAL
(p . lp) + ((lp . lp) + (- (lp . lp))) is V11() real ext-real Element of REAL
((p + lp) - lp) . lp is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(lp,p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lp + lp is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((lp + lp),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
f is set
seq_id f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
tseq is set
seq_id tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is Element of the carrier of Linear_Space_of_RealSequences
tv is Element of the carrier of Linear_Space_of_RealSequences
e + tv is Element of the carrier of Linear_Space_of_RealSequences
the addF of Linear_Space_of_RealSequences is non empty Relation-like [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] -defined the carrier of Linear_Space_of_RealSequences -valued Function-like V26([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:]) V30([: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences) Element of bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:]
[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] is non empty set
[:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
bool [:[: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:], the carrier of Linear_Space_of_RealSequences:] is non empty set
K473( the carrier of Linear_Space_of_RealSequences, the addF of Linear_Space_of_RealSequences,e,tv) is Element of the carrier of Linear_Space_of_RealSequences
[e,tv] is set
{e,tv} is non empty set
{e} is non empty set
{{e,tv},{e}} is non empty set
the addF of Linear_Space_of_RealSequences . [e,tv] is set
seq_id (e + tv) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id e is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id e) + (seq_id tv) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id ((seq_id e) + (seq_id tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
1 / p is V11() real ext-real Element of REAL
lp is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like NORMSTR
the carrier of lp is non empty set
[:NAT, the carrier of lp:] is non empty set
bool [:NAT, the carrier of lp:] is non empty set
lp is non empty Relation-like NAT -defined the carrier of lp -valued Function-like V26( NAT ) V30( NAT , the carrier of lp) Element of bool [:NAT, the carrier of lp:]
p * (1 / p) is V11() real ext-real Element of REAL
p * 1 is V11() real ext-real Element of REAL
(p * 1) / p is V11() real ext-real Element of REAL
f is set
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim tv is V11() real ext-real Element of REAL
e is V11() real ext-real set
e1 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
tv . m is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
tv . n is V11() real ext-real Element of REAL
(tv . n) - (tv . m) is V11() real ext-real Element of REAL
abs ((tv . n) - (tv . m)) is V11() real ext-real Element of REAL
lp . n is Element of the carrier of lp
lp . m is Element of the carrier of lp
(lp . n) - (lp . m) is Element of the carrier of lp
- (lp . m) is Element of the carrier of lp
(lp . n) + (- (lp . m)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,(lp . n),(- (lp . m))) is Element of the carrier of lp
[(lp . n),(- (lp . m))] is set
{(lp . n),(- (lp . m))} is non empty set
{(lp . n)} is non empty set
{{(lp . n),(- (lp . m))},{(lp . n)}} is non empty set
the addF of lp . [(lp . n),(- (lp . m))] is set
||.((lp . n) - (lp . m)).|| is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . ((lp . n) - (lp . m)) is V11() real ext-real Element of REAL
the normF of lp . ((lp . n) - (lp . m)) is V11() real ext-real Element of REAL
seq_id ((lp . n) - (lp . m)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id ((lp . n) - (lp . m))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id ((lp . n) - (lp . m))),p) is V11() real ext-real Element of REAL
(Sum ((seq_id ((lp . n) - (lp . m))),p)) to_power (1 / p) is V11() real ext-real Element of REAL
e1 to_power p is V11() real ext-real Element of REAL
((Sum ((seq_id ((lp . n) - (lp . m))),p)) to_power (1 / p)) to_power p is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id ((lp . n) - (lp . m))),p) . i is V11() real ext-real Element of REAL
(seq_id ((lp . n) - (lp . m))) . i is V11() real ext-real Element of REAL
abs ((seq_id ((lp . n) - (lp . m))) . i) is V11() real ext-real Element of REAL
(abs ((seq_id ((lp . n) - (lp . m))) . i)) to_power p is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
b * c is V11() real ext-real Element of REAL
m to_power (b * c) is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
m to_power b is V11() real ext-real Element of REAL
(m to_power b) to_power c is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
m to_power b is V11() real ext-real Element of REAL
(m to_power b) to_power c is V11() real ext-real Element of REAL
b * c is V11() real ext-real Element of REAL
m to_power (b * c) is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
m to_power b is V11() real ext-real Element of REAL
(m to_power b) to_power c is V11() real ext-real Element of REAL
b * c is V11() real ext-real Element of REAL
m to_power (b * c) is V11() real ext-real Element of REAL
((seq_id ((lp . n) - (lp . m))),p) . tseq is V11() real ext-real Element of REAL
(seq_id ((lp . n) - (lp . m))) . tseq is V11() real ext-real Element of REAL
abs ((seq_id ((lp . n) - (lp . m))) . tseq) is V11() real ext-real Element of REAL
(abs ((seq_id ((lp . n) - (lp . m))) . tseq)) to_power p is V11() real ext-real Element of REAL
(((seq_id ((lp . n) - (lp . m))),p) . tseq) to_power (1 / p) is V11() real ext-real Element of REAL
(abs ((seq_id ((lp . n) - (lp . m))) . tseq)) to_power 1 is V11() real ext-real Element of REAL
seq_id (lp . n) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . n)) . tseq is V11() real ext-real Element of REAL
(1 / p) * p is V11() real ext-real Element of REAL
(Sum ((seq_id ((lp . n) - (lp . m))),p)) to_power ((1 / p) * p) is V11() real ext-real Element of REAL
seq_id (lp . m) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . m)) . tseq is V11() real ext-real Element of REAL
i is Element of the carrier of lp
i is Element of the carrier of lp
i - i is Element of the carrier of lp
- i is Element of the carrier of lp
i + (- i) is Element of the carrier of lp
K473( the carrier of lp, the addF of lp,i,(- i)) is Element of the carrier of lp
[i,(- i)] is set
{i,(- i)} is non empty set
{i} is non empty set
{{i,(- i)},{i}} is non empty set
the addF of lp . [i,(- i)] is set
seq_id i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id i) - (seq_id i) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id i) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id i) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id i) + (- (seq_id i)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
- (seq_id (lp . m)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
K38(1) (#) (seq_id (lp . m)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id (lp . n)) + (- (seq_id (lp . m))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (lp . n)) + (- (seq_id (lp . m)))) . tseq is V11() real ext-real Element of REAL
abs (((seq_id (lp . n)) + (- (seq_id (lp . m)))) . tseq) is V11() real ext-real Element of REAL
(- (seq_id (lp . m))) . tseq is V11() real ext-real Element of REAL
((seq_id (lp . n)) . tseq) + ((- (seq_id (lp . m))) . tseq) is V11() real ext-real Element of REAL
abs (((seq_id (lp . n)) . tseq) + ((- (seq_id (lp . m))) . tseq)) is V11() real ext-real Element of REAL
- ((seq_id (lp . m)) . tseq) is V11() real ext-real Element of REAL
((seq_id (lp . n)) . tseq) + (- ((seq_id (lp . m)) . tseq)) is V11() real ext-real Element of REAL
abs (((seq_id (lp . n)) . tseq) + (- ((seq_id (lp . m)) . tseq))) is V11() real ext-real Element of REAL
(e1 to_power p) to_power (1 / p) is V11() real ext-real Element of REAL
e1 to_power ((1 / p) * p) is V11() real ext-real Element of REAL
e1 to_power 1 is V11() real ext-real Element of REAL
f is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
e is set
f . e is V11() real ext-real Element of REAL
tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq . tv is V11() real ext-real Element of REAL
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
m is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim m is V11() real ext-real Element of REAL
seq_id tseq is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . tv is Element of the carrier of lp
seq_id (lp . tv) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id (lp . tv)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id (lp . tv)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id tseq) + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id tseq) - (seq_id (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . e is Element of the carrier of lp
e1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . e1 is Element of the carrier of lp
(lp . e) - (lp . e1) is Element of the carrier of lp
- (lp . e1) is Element of the carrier of lp
(lp . e) + (- (lp . e1)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,(lp . e),(- (lp . e1))) is Element of the carrier of lp
[(lp . e),(- (lp . e1))] is set
{(lp . e),(- (lp . e1))} is non empty set
{(lp . e)} is non empty set
{{(lp . e),(- (lp . e1))},{(lp . e)}} is non empty set
the addF of lp . [(lp . e),(- (lp . e1))] is set
seq_id ((lp . e) - (lp . e1)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id (lp . e) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
seq_id (lp . e1) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . e)) - (seq_id (lp . e1)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id (lp . e1)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) (#) (seq_id (lp . e1)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id (lp . e)) + (- (seq_id (lp . e1))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
seq_id ((seq_id (lp . e)) - (seq_id (lp . e1))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . e is V11() real ext-real Element of REAL
e + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . (e + 1) is V11() real ext-real Element of REAL
e1 is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq . (e + 1) is V11() real ext-real Element of REAL
m is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim m is V11() real ext-real Element of REAL
n is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim n is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
n . i is V11() real ext-real Element of REAL
lp . i is Element of the carrier of lp
(lp . i) - (lp . tv) is Element of the carrier of lp
- (lp . tv) is Element of the carrier of lp
(lp . i) + (- (lp . tv)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,(lp . i),(- (lp . tv))) is Element of the carrier of lp
[(lp . i),(- (lp . tv))] is set
{(lp . i),(- (lp . tv))} is non empty set
{(lp . i)} is non empty set
{{(lp . i),(- (lp . tv))},{(lp . i)}} is non empty set
the addF of lp . [(lp . i),(- (lp . tv))] is set
seq_id ((lp . i) - (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id ((lp . i) - (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id ((lp . i) - (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums ((seq_id ((lp . i) - (lp . tv))),p)) . (e + 1) is V11() real ext-real Element of REAL
((seq_id ((lp . i) - (lp . tv))),p) . (e + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((seq_id ((lp . i) - (lp . tv))),p)) . e is V11() real ext-real Element of REAL
(((seq_id ((lp . i) - (lp . tv))),p) . (e + 1)) + ((Partial_Sums ((seq_id ((lp . i) - (lp . tv))),p)) . e) is V11() real ext-real Element of REAL
seq_id (lp . i) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . i)) - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . i)) + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id (lp . i)) - (seq_id (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(((seq_id (lp . i)) - (seq_id (lp . tv))),p) . (e + 1) is V11() real ext-real Element of REAL
((((seq_id (lp . i)) - (seq_id (lp . tv))),p) . (e + 1)) + ((Partial_Sums ((seq_id ((lp . i) - (lp . tv))),p)) . e) is V11() real ext-real Element of REAL
e1 . i is V11() real ext-real Element of REAL
((((seq_id (lp . i)) - (seq_id (lp . tv))),p) . (e + 1)) + (e1 . i) is V11() real ext-real Element of REAL
- (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . i)) + (- (seq_id (lp . tv))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (lp . i)) + (- (seq_id (lp . tv)))) . (e + 1) is V11() real ext-real Element of REAL
abs (((seq_id (lp . i)) + (- (seq_id (lp . tv)))) . (e + 1)) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . i)) + (- (seq_id (lp . tv)))) . (e + 1))) to_power p is V11() real ext-real Element of REAL
((abs (((seq_id (lp . i)) + (- (seq_id (lp . tv)))) . (e + 1))) to_power p) + (e1 . i) is V11() real ext-real Element of REAL
(seq_id (lp . i)) . (e + 1) is V11() real ext-real Element of REAL
(- (seq_id (lp . tv))) . (e + 1) is V11() real ext-real Element of REAL
((seq_id (lp . i)) . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1)) is V11() real ext-real Element of REAL
abs (((seq_id (lp . i)) . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1))) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . i)) . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1)))) to_power p is V11() real ext-real Element of REAL
((abs (((seq_id (lp . i)) . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1)))) to_power p) + (e1 . i) is V11() real ext-real Element of REAL
(seq_id (lp . tv)) . (e + 1) is V11() real ext-real Element of REAL
- ((seq_id (lp . tv)) . (e + 1)) is V11() real ext-real Element of REAL
((seq_id (lp . i)) . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1))) is V11() real ext-real Element of REAL
abs (((seq_id (lp . i)) . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1)))) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . i)) . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1))))) to_power p is V11() real ext-real Element of REAL
((abs (((seq_id (lp . i)) . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1))))) to_power p) + (e1 . i) is V11() real ext-real Element of REAL
((seq_id (lp . i)) . (e + 1)) - ((seq_id (lp . tv)) . (e + 1)) is V11() real ext-real Element of REAL
abs (((seq_id (lp . i)) . (e + 1)) - ((seq_id (lp . tv)) . (e + 1))) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . i)) . (e + 1)) - ((seq_id (lp . tv)) . (e + 1)))) to_power p is V11() real ext-real Element of REAL
((abs (((seq_id (lp . i)) . (e + 1)) - ((seq_id (lp . tv)) . (e + 1)))) to_power p) + (e1 . i) is V11() real ext-real Element of REAL
m . i is V11() real ext-real Element of REAL
(m . i) - ((seq_id (lp . tv)) . (e + 1)) is V11() real ext-real Element of REAL
abs ((m . i) - ((seq_id (lp . tv)) . (e + 1))) is V11() real ext-real Element of REAL
(abs ((m . i) - ((seq_id (lp . tv)) . (e + 1)))) to_power p is V11() real ext-real Element of REAL
((abs ((m . i) - ((seq_id (lp . tv)) . (e + 1)))) to_power p) + (e1 . i) is V11() real ext-real Element of REAL
lim e1 is V11() real ext-real Element of REAL
(lim m) - ((seq_id (lp . tv)) . (e + 1)) is V11() real ext-real Element of REAL
abs ((lim m) - ((seq_id (lp . tv)) . (e + 1))) is V11() real ext-real Element of REAL
(abs ((lim m) - ((seq_id (lp . tv)) . (e + 1)))) to_power p is V11() real ext-real Element of REAL
((abs ((lim m) - ((seq_id (lp . tv)) . (e + 1)))) to_power p) + (lim e1) is V11() real ext-real Element of REAL
(tseq . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1))) is V11() real ext-real Element of REAL
abs ((tseq . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1)))) is V11() real ext-real Element of REAL
(abs ((tseq . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1))))) to_power p is V11() real ext-real Element of REAL
((abs ((tseq . (e + 1)) + (- ((seq_id (lp . tv)) . (e + 1))))) to_power p) + (lim e1) is V11() real ext-real Element of REAL
(tseq . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1)) is V11() real ext-real Element of REAL
abs ((tseq . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1))) is V11() real ext-real Element of REAL
(abs ((tseq . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1)))) to_power p is V11() real ext-real Element of REAL
((abs ((tseq . (e + 1)) + ((- (seq_id (lp . tv))) . (e + 1)))) to_power p) + (lim e1) is V11() real ext-real Element of REAL
tseq - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(tseq - (seq_id (lp . tv))) . (e + 1) is V11() real ext-real Element of REAL
abs ((tseq - (seq_id (lp . tv))) . (e + 1)) is V11() real ext-real Element of REAL
(abs ((tseq - (seq_id (lp . tv))) . (e + 1))) to_power p is V11() real ext-real Element of REAL
((abs ((tseq - (seq_id (lp . tv))) . (e + 1))) to_power p) + (lim e1) is V11() real ext-real Element of REAL
((tseq - (seq_id (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((tseq - (seq_id (lp . tv))),p) . (e + 1) is V11() real ext-real Element of REAL
(((tseq - (seq_id (lp . tv))),p) . (e + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . e) is V11() real ext-real Element of REAL
(((seq_id tseq) - (seq_id (lp . tv))),p) . (e + 1) is V11() real ext-real Element of REAL
((((seq_id tseq) - (seq_id (lp . tv))),p) . (e + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . e) is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . e is V11() real ext-real Element of REAL
e1 is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e + 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lim e1 is V11() real ext-real Element of REAL
(Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . (e + 1) is V11() real ext-real Element of REAL
e is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim e is V11() real ext-real Element of REAL
(Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . 0 is V11() real ext-real Element of REAL
tseq . 0 is V11() real ext-real Element of REAL
e1 is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim e1 is V11() real ext-real Element of REAL
(seq_id (lp . tv)) . 0 is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
e . m is V11() real ext-real Element of REAL
e1 . m is V11() real ext-real Element of REAL
(e1 . m) - ((seq_id (lp . tv)) . 0) is V11() real ext-real Element of REAL
abs ((e1 . m) - ((seq_id (lp . tv)) . 0)) is V11() real ext-real Element of REAL
(abs ((e1 . m) - ((seq_id (lp . tv)) . 0))) to_power p is V11() real ext-real Element of REAL
lp . m is Element of the carrier of lp
(lp . m) - (lp . tv) is Element of the carrier of lp
- (lp . tv) is Element of the carrier of lp
(lp . m) + (- (lp . tv)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,(lp . m),(- (lp . tv))) is Element of the carrier of lp
[(lp . m),(- (lp . tv))] is set
{(lp . m),(- (lp . tv))} is non empty set
{(lp . m)} is non empty set
{{(lp . m),(- (lp . tv))},{(lp . m)}} is non empty set
the addF of lp . [(lp . m),(- (lp . tv))] is set
seq_id ((lp . m) - (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id ((lp . m) - (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id ((lp . m) - (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums ((seq_id ((lp . m) - (lp . tv))),p)) . 0 is V11() real ext-real Element of REAL
((seq_id ((lp . m) - (lp . tv))),p) . 0 is V11() real ext-real Element of REAL
seq_id (lp . m) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . m)) - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . m)) + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id (lp . m)) - (seq_id (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(((seq_id (lp . m)) - (seq_id (lp . tv))),p) . 0 is V11() real ext-real Element of REAL
- (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id (lp . m)) + (- (seq_id (lp . tv))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (lp . m)) + (- (seq_id (lp . tv)))) . 0 is V11() real ext-real Element of REAL
abs (((seq_id (lp . m)) + (- (seq_id (lp . tv)))) . 0) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . m)) + (- (seq_id (lp . tv)))) . 0)) to_power p is V11() real ext-real Element of REAL
(seq_id (lp . m)) . 0 is V11() real ext-real Element of REAL
(- (seq_id (lp . tv))) . 0 is V11() real ext-real Element of REAL
((seq_id (lp . m)) . 0) + ((- (seq_id (lp . tv))) . 0) is V11() real ext-real Element of REAL
abs (((seq_id (lp . m)) . 0) + ((- (seq_id (lp . tv))) . 0)) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . m)) . 0) + ((- (seq_id (lp . tv))) . 0))) to_power p is V11() real ext-real Element of REAL
- ((seq_id (lp . tv)) . 0) is V11() real ext-real Element of REAL
((seq_id (lp . m)) . 0) + (- ((seq_id (lp . tv)) . 0)) is V11() real ext-real Element of REAL
abs (((seq_id (lp . m)) . 0) + (- ((seq_id (lp . tv)) . 0))) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . m)) . 0) + (- ((seq_id (lp . tv)) . 0)))) to_power p is V11() real ext-real Element of REAL
((seq_id (lp . m)) . 0) - ((seq_id (lp . tv)) . 0) is V11() real ext-real Element of REAL
abs (((seq_id (lp . m)) . 0) - ((seq_id (lp . tv)) . 0)) is V11() real ext-real Element of REAL
(abs (((seq_id (lp . m)) . 0) - ((seq_id (lp . tv)) . 0))) to_power p is V11() real ext-real Element of REAL
(lim e1) - ((seq_id (lp . tv)) . 0) is V11() real ext-real Element of REAL
abs ((lim e1) - ((seq_id (lp . tv)) . 0)) is V11() real ext-real Element of REAL
(abs ((lim e1) - ((seq_id (lp . tv)) . 0))) to_power p is V11() real ext-real Element of REAL
- ((seq_id (lp . tv)) . 0) is V11() real ext-real Element of REAL
(tseq . 0) + (- ((seq_id (lp . tv)) . 0)) is V11() real ext-real Element of REAL
abs ((tseq . 0) + (- ((seq_id (lp . tv)) . 0))) is V11() real ext-real Element of REAL
(abs ((tseq . 0) + (- ((seq_id (lp . tv)) . 0)))) to_power p is V11() real ext-real Element of REAL
- (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(- (seq_id (lp . tv))) . 0 is V11() real ext-real Element of REAL
(tseq . 0) + ((- (seq_id (lp . tv))) . 0) is V11() real ext-real Element of REAL
abs ((tseq . 0) + ((- (seq_id (lp . tv))) . 0)) is V11() real ext-real Element of REAL
(abs ((tseq . 0) + ((- (seq_id (lp . tv))) . 0))) to_power p is V11() real ext-real Element of REAL
tseq - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tseq + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(tseq - (seq_id (lp . tv))) . 0 is V11() real ext-real Element of REAL
abs ((tseq - (seq_id (lp . tv))) . 0) is V11() real ext-real Element of REAL
(abs ((tseq - (seq_id (lp . tv))) . 0)) to_power p is V11() real ext-real Element of REAL
(seq_id tseq) + (- (seq_id (lp . tv))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id tseq) + (- (seq_id (lp . tv)))) . 0 is V11() real ext-real Element of REAL
abs (((seq_id tseq) + (- (seq_id (lp . tv)))) . 0) is V11() real ext-real Element of REAL
(abs (((seq_id tseq) + (- (seq_id (lp . tv)))) . 0)) to_power p is V11() real ext-real Element of REAL
(((seq_id tseq) + (- (seq_id (lp . tv)))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(((seq_id tseq) + (- (seq_id (lp . tv)))),p) . 0 is V11() real ext-real Element of REAL
e is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim e is V11() real ext-real Element of REAL
e1 is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lim e1 is V11() real ext-real Element of REAL
(Partial_Sums (((seq_id tseq) - (seq_id (lp . tv))),p)) . e is V11() real ext-real Element of REAL
tv is V11() real ext-real Element of REAL
tv / 2 is V11() real ext-real Element of REAL
(tv / 2) to_power (1 / p) is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . n is Element of the carrier of lp
lp . i is Element of the carrier of lp
(lp . n) - (lp . i) is Element of the carrier of lp
- (lp . i) is Element of the carrier of lp
(lp . n) + (- (lp . i)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,(lp . n),(- (lp . i))) is Element of the carrier of lp
[(lp . n),(- (lp . i))] is set
{(lp . n),(- (lp . i))} is non empty set
{(lp . n)} is non empty set
{{(lp . n),(- (lp . i))},{(lp . n)}} is non empty set
the addF of lp . [(lp . n),(- (lp . i))] is set
seq_id ((lp . n) - (lp . i)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id ((lp . n) - (lp . i))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id ((lp . n) - (lp . i))),p) is V11() real ext-real Element of REAL
||.((lp . n) - (lp . i)).|| is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . ((lp . n) - (lp . i)) is V11() real ext-real Element of REAL
the normF of lp . ((lp . n) - (lp . i)) is V11() real ext-real Element of REAL
(Sum ((seq_id ((lp . n) - (lp . i))),p)) to_power (1 / p) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id ((lp . n) - (lp . i))),p) . i is V11() real ext-real Element of REAL
(seq_id ((lp . n) - (lp . i))) . i is V11() real ext-real Element of REAL
abs ((seq_id ((lp . n) - (lp . i))) . i) is V11() real ext-real Element of REAL
(abs ((seq_id ((lp . n) - (lp . i))) . i)) to_power p is V11() real ext-real Element of REAL
((tv / 2) to_power (1 / p)) to_power p is V11() real ext-real Element of REAL
(1 / p) * p is V11() real ext-real Element of REAL
(tv / 2) to_power ((1 / p) * p) is V11() real ext-real Element of REAL
(tv / 2) to_power 1 is V11() real ext-real Element of REAL
((Sum ((seq_id ((lp . n) - (lp . i))),p)) to_power (1 / p)) to_power p is V11() real ext-real Element of REAL
(Sum ((seq_id ((lp . n) - (lp . i))),p)) to_power ((1 / p) * p) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id ((lp . n) - (lp . i))),p) . i is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . n is Element of the carrier of lp
seq_id (lp . n) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (lp . n)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id (lp . n)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id (lp . n)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id tseq) + (- (seq_id (lp . n))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id tseq) - (seq_id (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (((seq_id tseq) - (seq_id (lp . n))),p) is V11() real ext-real Element of REAL
Partial_Sums (((seq_id tseq) - (seq_id (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (lp . n))),p)) . i is V11() real ext-real Element of REAL
i is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
i . m is V11() real ext-real Element of REAL
lp . m is Element of the carrier of lp
(lp . m) - (lp . n) is Element of the carrier of lp
- (lp . n) is Element of the carrier of lp
(lp . m) + (- (lp . n)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,(lp . m),(- (lp . n))) is Element of the carrier of lp
[(lp . m),(- (lp . n))] is set
{(lp . m),(- (lp . n))} is non empty set
{(lp . m)} is non empty set
{{(lp . m),(- (lp . n))},{(lp . m)}} is non empty set
the addF of lp . [(lp . m),(- (lp . n))] is set
seq_id ((lp . m) - (lp . n)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id ((lp . m) - (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums ((seq_id ((lp . m) - (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Partial_Sums ((seq_id ((lp . m) - (lp . n))),p)) . i is V11() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
((seq_id ((lp . m) - (lp . n))),p) . b is V11() real ext-real Element of REAL
Sum ((seq_id ((lp . m) - (lp . n))),p) is V11() real ext-real Element of REAL
lim i is V11() real ext-real Element of REAL
(tv / 2) + 1 is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(Partial_Sums (((seq_id tseq) - (seq_id (lp . n))),p)) . i is V11() real ext-real Element of REAL
i is V11() real ext-real Element of REAL
lim (Partial_Sums (((seq_id tseq) - (seq_id (lp . n))),p)) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(((seq_id tseq) - (seq_id (lp . n))),p) . i is V11() real ext-real Element of REAL
((seq_id tseq) - (seq_id (lp . n))) . i is V11() real ext-real Element of REAL
abs (((seq_id tseq) - (seq_id (lp . n))) . i) is V11() real ext-real Element of REAL
(abs (((seq_id tseq) - (seq_id (lp . n))) . i)) to_power p is V11() real ext-real Element of REAL
((seq_id tseq),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . tv is Element of the carrier of lp
seq_id (lp . tv) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id (lp . tv)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id (lp . tv)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id tseq) + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id tseq) - (seq_id (lp . tv))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id tseq) - (seq_id (lp . tv))) + (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tseq) + (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id tseq) + (seq_id (lp . tv))) + (- (seq_id (lp . tv))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id tseq) + (seq_id (lp . tv))) - (seq_id (lp . tv)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id tseq) + (seq_id (lp . tv))) + (- (seq_id (lp . tv))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
((seq_id (lp . tv)),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
tv is Element of the carrier of lp
e is V11() real ext-real Element of REAL
e to_power p is V11() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
lp . n is Element of the carrier of lp
seq_id (lp . n) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tseq) - (seq_id (lp . n)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
- (seq_id (lp . n)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (seq_id (lp . n)) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(seq_id tseq) + (- (seq_id (lp . n))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id tseq) - (seq_id (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (((seq_id tseq) - (seq_id (lp . n))),p) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V52() V53() V54() V55() V56() V57() Element of NAT
(((seq_id tseq) - (seq_id (lp . n))),p) . i is V11() real ext-real Element of REAL
((seq_id tseq) - (seq_id (lp . n))) . i is V11() real ext-real Element of REAL
abs (((seq_id tseq) - (seq_id (lp . n))) . i) is V11() real ext-real Element of REAL
(abs (((seq_id tseq) - (seq_id (lp . n))) . i)) to_power p is V11() real ext-real Element of REAL
(e to_power p) to_power (1 / p) is V11() real ext-real Element of REAL
e to_power (p * (1 / p)) is V11() real ext-real Element of REAL
e to_power 1 is V11() real ext-real Element of REAL
seq_id tv is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tv) - (seq_id (lp . n)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(seq_id tv) + (- (seq_id (lp . n))) is Relation-like NAT -defined Function-like V26( NAT ) V33() V34() V35() set
(((seq_id tv) - (seq_id (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum (((seq_id tv) - (seq_id (lp . n))),p) is V11() real ext-real Element of REAL
(Sum (((seq_id tv) - (seq_id (lp . n))),p)) to_power (1 / p) is V11() real ext-real Element of REAL
seq_id ((seq_id tv) - (seq_id (lp . n))) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id ((seq_id tv) - (seq_id (lp . n)))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id ((seq_id tv) - (seq_id (lp . n)))),p) is V11() real ext-real Element of REAL
(Sum ((seq_id ((seq_id tv) - (seq_id (lp . n)))),p)) to_power (1 / p) is V11() real ext-real Element of REAL
tv - (lp . n) is Element of the carrier of lp
- (lp . n) is Element of the carrier of lp
tv + (- (lp . n)) is Element of the carrier of lp
the addF of lp is non empty Relation-like [: the carrier of lp, the carrier of lp:] -defined the carrier of lp -valued Function-like V26([: the carrier of lp, the carrier of lp:]) V30([: the carrier of lp, the carrier of lp:], the carrier of lp) Element of bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:]
[: the carrier of lp, the carrier of lp:] is non empty set
[:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
bool [:[: the carrier of lp, the carrier of lp:], the carrier of lp:] is non empty set
K473( the carrier of lp, the addF of lp,tv,(- (lp . n))) is Element of the carrier of lp
[tv,(- (lp . n))] is set
{tv,(- (lp . n))} is non empty set
{tv} is non empty set
{{tv,(- (lp . n))},{tv}} is non empty set
the addF of lp . [tv,(- (lp . n))] is set
seq_id (tv - (lp . n)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
((seq_id (tv - (lp . n))),p) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sum ((seq_id (tv - (lp . n))),p) is V11() real ext-real Element of REAL
(Sum ((seq_id (tv - (lp . n))),p)) to_power (1 / p) is V11() real ext-real Element of REAL
the normF of lp is non empty Relation-like the carrier of lp -defined REAL -valued Function-like V26( the carrier of lp) V30( the carrier of lp, REAL ) V33() V34() V35() Element of bool [: the carrier of lp,REAL:]
[: the carrier of lp,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of lp,REAL:] is non empty set
the normF of lp . (tv - (lp . n)) is V11() real ext-real Element of REAL
||.(tv + (- (lp . n))).|| is V11() real ext-real Element of REAL
the normF of lp . (tv + (- (lp . n))) is V11() real ext-real Element of REAL
(lp . n) - tv is Element of the carrier of lp
- tv is Element of the carrier of lp
(lp . n) + (- tv) is Element of the carrier of lp
K473( the carrier of lp, the addF of lp,(lp . n),(- tv)) is Element of the carrier of lp
[(lp . n),(- tv)] is set
{(lp . n),(- tv)} is non empty set
{(lp . n)} is non empty set
{{(lp . n),(- tv)},{(lp . n)}} is non empty set
the addF of lp . [(lp . n),(- tv)] is set
- ((lp . n) - tv) is Element of the carrier of lp
||.(- ((lp . n) - tv)).|| is V11() real ext-real Element of REAL
the normF of lp . (- ((lp . n) - tv)) is V11() real ext-real Element of REAL
||.((lp . n) - tv).|| is V11() real ext-real Element of REAL
the normF of lp . ((lp . n) - tv) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(p) is non empty Element of bool the carrier of Linear_Space_of_RealSequences
Zero_ ((p),Linear_Space_of_RealSequences) is Element of (p)
Add_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:(p),(p):] -defined (p) -valued Function-like V26([:(p),(p):]) V30([:(p),(p):],(p)) Element of bool [:[:(p),(p):],(p):]
[:(p),(p):] is non empty set
[:[:(p),(p):],(p):] is non empty set
bool [:[:(p),(p):],(p):] is non empty set
Mult_ ((p),Linear_Space_of_RealSequences) is non empty Relation-like [:REAL,(p):] -defined (p) -valued Function-like V26([:REAL,(p):]) V30([:REAL,(p):],(p)) Element of bool [:[:REAL,(p):],(p):]
[:REAL,(p):] is non empty set
[:[:REAL,(p):],(p):] is non empty set
bool [:[:REAL,(p):],(p):] is non empty set
(p) is non empty Relation-like (p) -defined REAL -valued Function-like V26((p)) V30((p), REAL ) V33() V34() V35() Element of bool [:(p),REAL:]
[:(p),REAL:] is non empty V33() V34() V35() set
bool [:(p),REAL:] is non empty set
NORMSTR(# (p),(Zero_ ((p),Linear_Space_of_RealSequences)),(Add_ ((p),Linear_Space_of_RealSequences)),(Mult_ ((p),Linear_Space_of_RealSequences)),(p) #) is strict NORMSTR
lp is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed discerning reflexive RealNormSpace-like NORMSTR
the carrier of lp is non empty set
[:NAT, the carrier of lp:] is non empty set
bool [:NAT, the carrier of lp:] is non empty set
f is non empty Relation-like NAT -defined the carrier of lp -valued Function-like V26( NAT ) V30( NAT , the carrier of lp) Element of bool [:NAT, the carrier of lp:]