set l1 = linfty_Space ;
A1: 0. linfty_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def 10
.= Zeroseq ;
A2: for x being set holds
( x is Element of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) )

proof

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

end;

A3: for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v)

proof

let u, v be VECTOR of linfty_Space; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm3, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_BoundedRealSequences ;
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 A4: dom ( the addF of Linear_Space_of_RealSequences || the_set_of_BoundedRealSequences) = [:the_set_of_BoundedRealSequences,the_set_of_BoundedRealSequences:] by RELAT_1:62;
u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_BoundedRealSequences) . [u,v] by RSSPACE:def 8
.= u1 + v1 by A4, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2; :: thesis: verum

end;

A5: for r being Real
for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u)

proof

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

end;

A7: for u being VECTOR of linfty_Space holds u = seq_id u

proof

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

end;

A8: for u being VECTOR of linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )

proof

let u be VECTOR of linfty_Space; :: thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1) * u by RLVECT_1:16
.= - (seq_id u) by A5 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ; :: thesis: verum

end;

for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v)

proof

let u, v be VECTOR of linfty_Space; :: thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A3
.= (seq_id u) - (seq_id v) by A8 ; :: thesis: verum

end;

hence ( the carrier of linfty_Space = the_set_of_BoundedRealSequences & ( for x being set holds
( x is VECTOR of linfty_Space iff ( x is Real_Sequence & seq_id x is bounded ) ) ) & 0. linfty_Space = Zeroseq & ( for u being VECTOR of linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of linfty_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of linfty_Space holds ||.v.|| = upper_bound (rng (abs (seq_id v))) ) ) by A2, A7, A3, A5, A8, A1, Def2; :: thesis: verum