set l1 = l1_Space ;
A1: for x being set holds
( x is Element of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) )

proof

let x be set ; :: thesis: ( x is Element of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) )
( x in the_set_of_RealSequences iff x is Real_Sequence ) by FUNCT_2:8, FUNCT_2:66;
hence ( x is Element of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) ) by Def1; :: thesis: verum

end;

A2: for u, v being VECTOR of l1_Space holds u + v = (seq_id u) + (seq_id v)

proof

let u, v be VECTOR of l1_Space; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_l1RealSequences ;
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 dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l1RealSequences) = [:the_set_of_l1RealSequences,the_set_of_l1RealSequences:] by RELAT_1:62, ZFMISC_1:96;
then A3: [u,v] in dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l1RealSequences) by ZFMISC_1:87;
u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_l1RealSequences) . [u,v] by RSSPACE:def 8
.= u1 + v1 by A3, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2; :: thesis: verum

end;

A4: for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u)

proof

let r be Real; :: thesis: for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of l1_Space; :: thesis: r * u = r (#) (seq_id u)
reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_l1RealSequences ;
dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;
then dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l1RealSequences:]) = [:REAL,the_set_of_l1RealSequences:] by RELAT_1:62, ZFMISC_1:96;
then A5: [r,u] in dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l1RealSequences:]) by ZFMISC_1:87;
r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l1RealSequences:]) . [r,u] by RSSPACE:def 9
.= r * u1 by A5, FUNCT_1:47 ;
hence r * u = r (#) (seq_id u) by RSSPACE:3; :: thesis: verum

end;

A6: for u being VECTOR of l1_Space holds u = seq_id u

proof

let u be VECTOR of l1_Space; :: thesis: u = seq_id u
u is VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10;
hence u = seq_id u ; :: thesis: verum

end;

A7: for u being VECTOR of l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )

proof

let u be VECTOR of l1_Space; :: thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1) * u by Th5, RLVECT_1:16
.= (- 1) (#) (seq_id u) by A4
.= - (seq_id u) by SEQ_1:17 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ; :: thesis: verum

end;

A8: for u, v being VECTOR of l1_Space holds u - v = (seq_id u) - (seq_id v)

proof

let u, v be VECTOR of l1_Space; :: thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A2
.= (seq_id u) + (- (seq_id v)) by A7
.= (seq_id u) - (seq_id v) by SEQ_1:11 ; :: thesis: verum

end;

A9: for v being VECTOR of l1_Space holds ||.v.|| = Sum (abs (seq_id v)) by Def2;
0. l1_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def 10
.= Zeroseq ;
hence ( the carrier of l1_Space = the_set_of_l1RealSequences & ( for x being set holds
( x is VECTOR of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) ) ) & 0. l1_Space = Zeroseq & ( for u being VECTOR of l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of l1_Space holds ||.v.|| = Sum (abs (seq_id v)) ) ) by A1, A6, A2, A4, A7, A8, A9; :: thesis: verum