let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) )

assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

let lp be non empty NORMSTR ; :: thesis: ( lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) implies ( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) )

assume A2: lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) ; :: thesis: ( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

A3: for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3;

A4: for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y)

for x being VECTOR of lp holds r * x = r (#) (seq_id x)

then A9: 0. lp = 0. Linear_Space_of_RealSequences by A2, RSSPACE:def 10

.= Zeroseq ;

A10: for x being set holds

( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )

x = seq_id x

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) by A2, A10, A11, A9, A4, A7, A12, A3; :: thesis: verum

( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) )

assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

let lp be non empty NORMSTR ; :: thesis: ( lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) implies ( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) )

assume A2: lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) ; :: thesis: ( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

A3: for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3;

A4: for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y)

proof

A7:
for r being Real
let x, y be VECTOR of lp; :: thesis: x + y = (seq_id x) + (seq_id y)

A5: lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10;

reconsider y1 = y as VECTOR of Linear_Space_of_RealSequences by A5, RLSUB_1:10;

set L1 = Linear_Space_of_RealSequences ;

set W = the_set_of_RealSequences_l^ p;

dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;

then A6: dom ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) = [:(the_set_of_RealSequences_l^ p),(the_set_of_RealSequences_l^ p):] by RELAT_1:62;

the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;

then x + y = ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) . [x,y] by A2, RSSPACE:def 8

.= x1 + y1 by A2, A6, FUNCT_1:47 ;

hence x + y = (seq_id x) + (seq_id y) by RSSPACE:2; :: thesis: verum

end;A5: lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10;

reconsider y1 = y as VECTOR of Linear_Space_of_RealSequences by A5, RLSUB_1:10;

set L1 = Linear_Space_of_RealSequences ;

set W = the_set_of_RealSequences_l^ p;

dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;

then A6: dom ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) = [:(the_set_of_RealSequences_l^ p),(the_set_of_RealSequences_l^ p):] by RELAT_1:62;

the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;

then x + y = ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) . [x,y] by A2, RSSPACE:def 8

.= x1 + y1 by A2, A6, FUNCT_1:47 ;

hence x + y = (seq_id x) + (seq_id y) by RSSPACE:2; :: thesis: verum

for x being VECTOR of lp holds r * x = r (#) (seq_id x)

proof

the_set_of_RealSequences_l^ p is linearly-closed
by A1, Th4;
set W = the_set_of_RealSequences_l^ p;

set L1 = Linear_Space_of_RealSequences ;

let r be Real; :: thesis: for x being VECTOR of lp holds r * x = r (#) (seq_id x)

reconsider r = r as Element of REAL by XREAL_0:def 1;

let x be VECTOR of lp; :: thesis: r * x = r (#) (seq_id x)

dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;

then A8: dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) = [:REAL,(the_set_of_RealSequences_l^ p):] by RELAT_1:62, ZFMISC_1:96;

lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10;

the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;

then r * x = ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) . [r,x] by A2, RSSPACE:def 9

.= r * x1 by A2, A8, FUNCT_1:47 ;

hence r * x = r (#) (seq_id x) by RSSPACE:3; :: thesis: verum

end;set L1 = Linear_Space_of_RealSequences ;

let r be Real; :: thesis: for x being VECTOR of lp holds r * x = r (#) (seq_id x)

reconsider r = r as Element of REAL by XREAL_0:def 1;

let x be VECTOR of lp; :: thesis: r * x = r (#) (seq_id x)

dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;

then A8: dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) = [:REAL,(the_set_of_RealSequences_l^ p):] by RELAT_1:62, ZFMISC_1:96;

lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10;

the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;

then r * x = ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) . [r,x] by A2, RSSPACE:def 9

.= r * x1 by A2, A8, FUNCT_1:47 ;

hence r * x = r (#) (seq_id x) by RSSPACE:3; :: thesis: verum

then A9: 0. lp = 0. Linear_Space_of_RealSequences by A2, RSSPACE:def 10

.= Zeroseq ;

A10: for x being set holds

( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )

proof

A11:
for x being set st x is VECTOR of lp holds
let x be set ; :: thesis: ( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )

( x in the_set_of_RealSequences_l^ p iff ( (seq_id x) rto_power p is summable & x in the_set_of_RealSequences ) ) by A1, Def2;

hence ( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) by A2, FUNCT_2:8, FUNCT_2:66; :: thesis: verum

end;( x in the_set_of_RealSequences_l^ p iff ( (seq_id x) rto_power p is summable & x in the_set_of_RealSequences ) ) by A1, Def2;

hence ( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) by A2, FUNCT_2:8, FUNCT_2:66; :: thesis: verum

x = seq_id x

proof

A12:
for x being VECTOR of lp holds
let x be set ; :: thesis: ( x is VECTOR of lp implies x = seq_id x )

( x in the_set_of_RealSequences iff x is Real_Sequence ) by FUNCT_2:8, FUNCT_2:66;

hence ( x is VECTOR of lp implies x = seq_id x ) by A1, A2, Def2; :: thesis: verum

end;( x in the_set_of_RealSequences iff x is Real_Sequence ) by FUNCT_2:8, FUNCT_2:66;

hence ( x is VECTOR of lp implies x = seq_id x ) by A1, A2, Def2; :: thesis: verum

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )

proof

for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y)
let x be VECTOR of lp; :: thesis: ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )

lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

then - x = (- 1) * x by RLVECT_1:16

.= - (seq_id x) by A7 ;

hence ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ; :: thesis: verum

end;lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;

then - x = (- 1) * x by RLVECT_1:16

.= - (seq_id x) by A7 ;

hence ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ; :: thesis: verum

proof

hence
( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds
let x, y be VECTOR of lp; :: thesis: x - y = (seq_id x) - (seq_id y)

thus x - y = (seq_id x) + (seq_id (- y)) by A4

.= (seq_id x) - (seq_id y) by A12 ; :: thesis: verum

end;thus x - y = (seq_id x) + (seq_id (- y)) by A4

.= (seq_id x) - (seq_id y) by A12 ; :: thesis: verum

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) by A2, A10, A11, A9, A4, A7, A12, A3; :: thesis: verum