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

proof

let x be set ; :: thesis: ( x is Element of iff ( x is Real_Sequence & seq_id x is bounded ) )
( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def 1;
hence ( x is Element of iff ( x is Real_Sequence & seq_id x is bounded ) ) by Def1; :: thesis: verum

end;

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

proof

let u, v be VECTOR of ; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of by Lm3, RLSUB_1:18;
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:91;
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:70 ;
hence u + v = (seq_id u) + (seq_id v) by RSSPACE:4, RSSPACE:def 7; :: thesis: verum

end;

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

proof

let r be Real; :: thesis: for u being VECTOR of holds r * u = r (#) (seq_id u)
let u be VECTOR of ; :: thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of by Lm3, RLSUB_1:18;
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:91, ZFMISC_1:119;
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:70 ;
hence r * u = r (#) (seq_id u) by RSSPACE:5, RSSPACE:def 7; :: thesis: verum

end;

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

proof

let u be VECTOR of ; :: thesis: u = seq_id u
u is VECTOR of by Lm3, RLSUB_1:18;
hence u = seq_id u by RSSPACE:def 2, RSSPACE:def 7; :: thesis: verum

end;

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

proof

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

end;

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

proof

let u, v be VECTOR of ; :: 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 iff ( x is Real_Sequence & seq_id x is bounded ) ) ) & 0. linfty_Space = Zeroseq & ( for u being VECTOR of holds u = seq_id u ) & ( for u, v being VECTOR of holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of holds seq_id v is bounded ) & ( for v being VECTOR of holds ||.v.|| = sup (rng (abs (seq_id v))) ) ) by A2, A7, A3, A5, A8, A1, Def2; :: thesis: verum