:: RSSPACE semantic presentation

begin

definition
func the_set_of_RealSequences  ->  non empty set  means :Def1: :: RSSPACE:def 1
 for x being set holds
( x in it iff x is Real_Sequence );
existence
 ex b1 being non empty set st
for x being set holds
( x in b1 iff x is Real_Sequence )
proof
defpred S1[ set ] means $1 is Real_Sequence;
consider IT being set  such that
A1: for x being set holds
( x in IT iff ( x in Funcs (NAT,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
 not IT is empty
proof
set zeroseq = the Real_Sequence;
 the Real_Sequence in Funcs (NAT,REAL) by FUNCT_2:8;
hence  not IT is empty by A1; ::_thesis: verum
end;
then reconsider IT = IT as non empty set ;
take  IT ; ::_thesis: for x being set holds
( x in IT iff x is Real_Sequence )
 for x being set st x is Real_Sequence holds
x in IT
proof
let x be set ; ::_thesis: ( x is Real_Sequence implies x in IT )
assume A2: x is Real_Sequence ; ::_thesis: x in IT
then  x in Funcs (NAT,REAL) by FUNCT_2:8;
hence  x in IT by A1, A2; ::_thesis: verum
end;
hence  for x being set holds
( x in IT iff x is Real_Sequence ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff x is Real_Sequence ) ) & ( for x being set holds
( x in b2 iff x is Real_Sequence ) ) holds
b1 = b2
proof
let X1, X2 be non empty set ; ::_thesis: ( ( for x being set holds
( x in X1 iff x is Real_Sequence ) ) & ( for x being set holds
( x in X2 iff x is Real_Sequence ) ) implies X1 = X2 )
assume that
A3: for x being set holds
( x in X1 iff x is Real_Sequence ) and
A4: for x being set holds
( x in X2 iff x is Real_Sequence ) ; ::_thesis: X1 = X2
A5: X2 c= X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 )
assume  x in X2 ; ::_thesis: x in X1
then  x is Real_Sequence by A4;
hence  x in X1 by A3; ::_thesis: verum
end;
 X1 c= X2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume  x in X1 ; ::_thesis: x in X2
then  x is Real_Sequence by A3;
hence  x in X2 by A4; ::_thesis: verum
end;
hence  X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def_1_:_
 for b1 being non empty set holds
( b1 = the_set_of_RealSequences iff for x being set holds
( x in b1 iff x is Real_Sequence ) );

definition
let a be set ;
assume A1: a in the_set_of_RealSequences ;
func seq_id a ->  Real_Sequence equals :Def2: :: RSSPACE:def 2
a;
coherence
 a is Real_Sequence by A1, Def1;
end;

:: deftheorem Def2 defines seq_id RSSPACE:def_2_:_
 for a being set st a in the_set_of_RealSequences holds
seq_id a = a;

definition
let a be set ;
assume A1: a in REAL ;
func R_id a ->  Real equals :Def3: :: RSSPACE:def 3
a;
coherence
 a is Real by A1;
end;

:: deftheorem Def3 defines R_id RSSPACE:def_3_:_
 for a being set st a in REAL holds
R_id a = a;

definition
func l_add  ->  BinOp of the_set_of_RealSequences means :Def4: :: RSSPACE:def 4
 for a, b being Element of the_set_of_RealSequences holds it . (a,b) = (seq_id a) + (seq_id b);
existence
 ex b1 being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b)
proof
defpred S1[ Element of the_set_of_RealSequences , Element of the_set_of_RealSequences , Element of the_set_of_RealSequences ] means $3 = (seq_id $1) + (seq_id $2);
A1: for x, y being Element of the_set_of_RealSequences ex z being Element of the_set_of_RealSequences st S1[x,y,z]
proof
let x, y be Element of the_set_of_RealSequences ; ::_thesis: ex z being Element of the_set_of_RealSequences st S1[x,y,z]
 (seq_id x) + (seq_id y) is Element of the_set_of_RealSequences by Def1;
hence  ex z being Element of the_set_of_RealSequences st S1[x,y,z] ; ::_thesis: verum
end;
 ex ADD being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds S1[a,b,ADD . (a,b)] from BINOP_1:sch_3(A1);
then consider ADD being BinOp of the_set_of_RealSequences such that
A2: for a, b being Element of the_set_of_RealSequences holds ADD . (a,b) = (seq_id a) + (seq_id b) ;
thus  ex b1 being BinOp of the_set_of_RealSequences st
for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of the_set_of_RealSequences st ( for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_RealSequences holds b2 . (a,b) = (seq_id a) + (seq_id b) ) holds
b1 = b2
proof
deffunc H1( Element of the_set_of_RealSequences , Element of the_set_of_RealSequences ) ->  Element of bool [:NAT,REAL:] = (seq_id $1) + (seq_id $2);
 for o1, o2 being BinOp of the_set_of_RealSequences st ( for a, b being Element of the_set_of_RealSequences holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of the_set_of_RealSequences holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2();
hence  for b1, b2 being BinOp of the_set_of_RealSequences st ( for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_RealSequences holds b2 . (a,b) = (seq_id a) + (seq_id b) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines l_add RSSPACE:def_4_:_
 for b1 being BinOp of the_set_of_RealSequences holds
( b1 = l_add iff for a, b being Element of the_set_of_RealSequences holds b1 . (a,b) = (seq_id a) + (seq_id b) );

definition
func l_mult  ->  Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences means :Def5: :: RSSPACE:def 5
 for r, x being set st r in REAL & x in the_set_of_RealSequences holds
it . (r,x) = (R_id r) (#) (seq_id x);
existence
 ex b1 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x)
proof
deffunc H1( set , set ) ->  Element of bool [:NAT,REAL:] = (R_id $1) (#) (seq_id $2);
A1: for r, x being set st r in REAL & x in the_set_of_RealSequences holds
H1(r,x) in the_set_of_RealSequences by Def1;
 ex f being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
f . (r,x) = H1(r,x) from BINOP_1:sch_2(A1);
hence  ex b1 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences st
for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences st ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b2 . (r,x) = (R_id r) (#) (seq_id x) ) holds
b1 = b2
proof
let mult1, mult2 be Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences; ::_thesis: ( ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult1 . (r,x) = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult2 . (r,x) = (R_id r) (#) (seq_id x) ) implies mult1 = mult2 )
assume that
A2: for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult1 . (r,x) = (R_id r) (#) (seq_id x) and
A3: for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult2 . (r,x) = (R_id r) (#) (seq_id x) ; ::_thesis: mult1 = mult2
 for r being Element of REAL
for x being Element of the_set_of_RealSequences holds mult1 . (r,x) = mult2 . (r,x)
proof
let r be Element of REAL ; ::_thesis: for x being Element of the_set_of_RealSequences holds mult1 . (r,x) = mult2 . (r,x)
let x be Element of the_set_of_RealSequences ; ::_thesis: mult1 . (r,x) = mult2 . (r,x)
thus mult1 . (r,x) = (R_id r) (#) (seq_id x) by A2
.= mult2 . (r,x) by A3 ; ::_thesis: verum
end;
hence  mult1 = mult2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines l_mult RSSPACE:def_5_:_
 for b1 being Function of [:REAL,the_set_of_RealSequences:],the_set_of_RealSequences holds
( b1 = l_mult iff for r, x being set st r in REAL & x in the_set_of_RealSequences holds
b1 . (r,x) = (R_id r) (#) (seq_id x) );

definition
func Zeroseq  ->  Element of the_set_of_RealSequences  means :Def6: :: RSSPACE:def 6
 for n being Element of NAT holds (seq_id it) . n = 0 ;
existence
 ex b1 being Element of the_set_of_RealSequences st
for n being Element of NAT holds (seq_id b1) . n = 0
proof
reconsider zeroseq = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
 zeroseq in the_set_of_RealSequences by Def1;
then A1: seq_id zeroseq = zeroseq by Def2;
reconsider zeroseq = zeroseq as Element of the_set_of_RealSequences by Def1;
take  zeroseq ; ::_thesis: for n being Element of NAT holds (seq_id zeroseq) . n = 0
let n be Nat; ::_thesis: ( n is Element of REAL & n is Element of NAT implies (seq_id zeroseq) . n = 0 )
thus  ( n is Element of REAL & n is Element of NAT implies (seq_id zeroseq) . n = 0 ) by A1, FUNCOP_1:7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of the_set_of_RealSequences st ( for n being Element of NAT holds (seq_id b1) . n = 0 ) & ( for n being Element of NAT holds (seq_id b2) . n = 0 ) holds
b1 = b2
proof
let x, y be Element of the_set_of_RealSequences ; ::_thesis: ( ( for n being Element of NAT holds (seq_id x) . n = 0 ) & ( for n being Element of NAT holds (seq_id y) . n = 0 ) implies x = y )
assume that
A2: for n being Element of NAT holds (seq_id x) . n = 0 and
A3: for n being Element of NAT holds (seq_id y) . n = 0 ; ::_thesis: x = y
A4: for s being set st s in NAT holds
(seq_id x) . s = (seq_id y) . s
proof
let s be set ; ::_thesis: ( s in NAT implies (seq_id x) . s = (seq_id y) . s )
assume A5: s in NAT ; ::_thesis: (seq_id x) . s = (seq_id y) . s
then  (seq_id y) . s = 0 by A3;
hence  (seq_id x) . s = (seq_id y) . s by A2, A5; ::_thesis: verum
end;
x = seq_id x by Def2
.= seq_id y by A4, FUNCT_2:12 ;
hence  x = y by Def2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Zeroseq RSSPACE:def_6_:_
 for b1 being Element of the_set_of_RealSequences holds
( b1 = Zeroseq iff for n being Element of NAT holds (seq_id b1) . n = 0 );

theorem Th1: :: RSSPACE:1
for x being Real_Sequence holds seq_id x = x
proof
let x be Real_Sequence; ::_thesis: seq_id x = x
reconsider x1 = x as set ;
 x1 in the_set_of_RealSequences by Def1;
hence  seq_id x = x by Def2; ::_thesis: verum
end;

theorem :: RSSPACE:2
for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds v + w = (seq_id v) + (seq_id w) by Def4;

theorem Th3: :: RSSPACE:3
for r being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds r * v = r (#) (seq_id v)
proof
let r be Real; ::_thesis: for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds r * v = r (#) (seq_id v)
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: r * v = r (#) (seq_id v)
thus r * v = (R_id r) (#) (seq_id v) by Def5
.= r (#) (seq_id v) by Def3 ; ::_thesis: verum
end;

registration
cluster RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) ->  Abelian ;
coherence
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is Abelian
proof
let v, w be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
 v + w = (seq_id v) + (seq_id w) by Def4;
hence  v + w = w + v by Def4; ::_thesis: verum
end;
end;

theorem Th4: :: RSSPACE:4
for u, v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: (u + v) + w = u + (v + w)
(u + v) + w = (seq_id (u + v)) + (seq_id w) by Def4
.= (seq_id ((seq_id u) + (seq_id v))) + (seq_id w) by Def4
.= ((seq_id u) + (seq_id v)) + (seq_id w) by Th1
.= (seq_id u) + ((seq_id v) + (seq_id w)) by SEQ_1:13
.= (seq_id u) + (seq_id ((seq_id v) + (seq_id w))) by Th1
.= (seq_id u) + (seq_id (v + w)) by Def4 ;
hence  (u + v) + w = u + (v + w) by Def4; ::_thesis: verum
end;

theorem Th5: :: RSSPACE:5
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = v
proof
set V = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = v
A1: for s being set st s in NAT holds
((seq_id v) + (seq_id Zeroseq)) . s = (seq_id v) . s
proof
let s be set ; ::_thesis: ( s in NAT implies ((seq_id v) + (seq_id Zeroseq)) . s = (seq_id v) . s )
assume A2: s in NAT ; ::_thesis: ((seq_id v) + (seq_id Zeroseq)) . s = (seq_id v) . s
((seq_id v) + (seq_id Zeroseq)) . s = ((seq_id v) . s) + ((seq_id Zeroseq) . s) by A2, SEQ_1:7
.= ((seq_id v) . s) + 0 by A2, Def6 ;
hence  ((seq_id v) + (seq_id Zeroseq)) . s = (seq_id v) . s ; ::_thesis: verum
end;
 v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = (seq_id v) + (seq_id Zeroseq) by Def4;
hence v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = seq_id v by A1, FUNCT_2:12
.= v by Def2 ;
::_thesis: verum
end;

theorem Th6: :: RSSPACE:6
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) ex w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
proof
set V = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: ex w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
reconsider w = - (seq_id v) as VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) by Def1;
 for s being set st s in NAT holds
((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s
proof
let s be set ; ::_thesis: ( s in NAT implies ((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s )
assume A1: s in NAT ; ::_thesis: ((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s
((seq_id v) + (- (seq_id v))) . s = ((seq_id v) . s) + ((- (seq_id v)) . s) by A1, SEQ_1:7
.= ((seq_id v) . s) + (- ((seq_id v) . s)) by A1, SEQ_1:10
.= (seq_id Zeroseq) . s by A1, Def6 ;
hence  ((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s ; ::_thesis: verum
end;
then A2: (seq_id v) + (- (seq_id v)) = seq_id Zeroseq by FUNCT_2:12
.= Zeroseq by Def2 ;
v + w = (seq_id v) + (seq_id w) by Def4
.= (seq_id v) + (- (seq_id v)) by Th1 ;
hence  ex w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) by A2; ::_thesis: verum
end;

theorem Th7: :: RSSPACE:7
for a being Real
for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds a * (v + w) = (a * v) + (a * w)
proof
let a be Real; ::_thesis: for v, w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: a * (v + w) = (a * v) + (a * w)
A1: a * (v + w) = a (#) (seq_id (v + w)) by Th3
.= a (#) (seq_id ((seq_id v) + (seq_id w))) by Def4
.= a (#) ((seq_id v) + (seq_id w)) by Th1
.= (a (#) (seq_id v)) + (a (#) (seq_id w)) by SEQ_1:22 ;
(a * v) + (a * w) = (seq_id (a * v)) + (seq_id (a * w)) by Def4
.= (seq_id (a (#) (seq_id v))) + (seq_id (a * w)) by Th3
.= (seq_id (a (#) (seq_id v))) + (seq_id (a (#) (seq_id w))) by Th3
.= (a (#) (seq_id v)) + (seq_id (a (#) (seq_id w))) by Th1
.= (a (#) (seq_id v)) + (a (#) (seq_id w)) by Th1 ;
hence  a * (v + w) = (a * v) + (a * w) by A1; ::_thesis: verum
end;

theorem Th8: :: RSSPACE:8
for a, b being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be Real; ::_thesis: for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: (a + b) * v = (a * v) + (b * v)
 for s being set st s in NAT holds
((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s
proof
let s be set ; ::_thesis: ( s in NAT implies ((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s )
assume A1: s in NAT ; ::_thesis: ((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s
((a + b) (#) (seq_id v)) . s = (a + b) * ((seq_id v) . s) by A1, SEQ_1:9
.= (a * ((seq_id v) . s)) + (b * ((seq_id v) . s))
.= ((a (#) (seq_id v)) . s) + (b * ((seq_id v) . s)) by A1, SEQ_1:9
.= ((a (#) (seq_id v)) . s) + ((b (#) (seq_id v)) . s) by A1, SEQ_1:9 ;
hence  ((a + b) (#) (seq_id v)) . s = ((a (#) (seq_id v)) + (b (#) (seq_id v))) . s by A1, SEQ_1:7; ::_thesis: verum
end;
then A2: (a + b) (#) (seq_id v) = (a (#) (seq_id v)) + (b (#) (seq_id v)) by FUNCT_2:12;
(a * v) + (b * v) = (seq_id (a * v)) + (seq_id (b * v)) by Def4
.= (seq_id (a (#) (seq_id v))) + (seq_id (b * v)) by Th3
.= (seq_id (a (#) (seq_id v))) + (seq_id (b (#) (seq_id v))) by Th3
.= (a (#) (seq_id v)) + (seq_id (b (#) (seq_id v))) by Th1
.= (a (#) (seq_id v)) + (b (#) (seq_id v)) by Th1 ;
hence  (a + b) * v = (a * v) + (b * v) by A2, Th3; ::_thesis: verum
end;

theorem Th9: :: RSSPACE:9
for a, b being Real
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a * b) * v = a * (b * v)
proof
let a, b be Real; ::_thesis: for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a * b) * v = a * (b * v)
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: (a * b) * v = a * (b * v)
(a * b) * v = (a * b) (#) (seq_id v) by Th3
.= a (#) (b (#) (seq_id v)) by SEQ_1:23
.= a (#) (seq_id (b (#) (seq_id v))) by Th1
.= a (#) (seq_id (b * v)) by Th3 ;
hence  (a * b) * v = a * (b * v) by Th3; ::_thesis: verum
end;

theorem Th10: :: RSSPACE:10
for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds 1 * v = v
proof
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); ::_thesis: 1 * v = v
1 * v = 1 (#) (seq_id v) by Th3
.= seq_id v by SEQ_1:27 ;
hence  1 * v = v by Def2; ::_thesis: verum
end;

definition
func Linear_Space_of_RealSequences  ->  RLSStruct  equals :: RSSPACE:def 7
 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
correctness
coherence
RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) is RLSStruct ;
;
end;

:: deftheorem  defines Linear_Space_of_RealSequences RSSPACE:def_7_:_
 Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

registration
cluster Linear_Space_of_RealSequences  ->  non empty strict ;
coherence
 ( Linear_Space_of_RealSequences is strict & not Linear_Space_of_RealSequences is empty ) ;
end;

registration
cluster Linear_Space_of_RealSequences  ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( Linear_Space_of_RealSequences is Abelian & Linear_Space_of_RealSequences is add-associative & Linear_Space_of_RealSequences is right_zeroed & Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof
set S = Linear_Space_of_RealSequences ;
thus  Linear_Space_of_RealSequences is Abelian ; ::_thesis: ( Linear_Space_of_RealSequences is add-associative & Linear_Space_of_RealSequences is right_zeroed & Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
thus  Linear_Space_of_RealSequences is add-associative ::_thesis: ( Linear_Space_of_RealSequences is right_zeroed & Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof
let u, v, w be Element of Linear_Space_of_RealSequences; :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
thus  (u + v) + w = u + (v + w) by Th4; ::_thesis: verum
end;
thus  Linear_Space_of_RealSequences is right_zeroed ::_thesis: ( Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof
let v be Element of Linear_Space_of_RealSequences; :: according to RLVECT_1:def_4 ::_thesis: v + (0. Linear_Space_of_RealSequences) = v
thus  v + (0. Linear_Space_of_RealSequences) = v by Th5; ::_thesis: verum
end;
thus  Linear_Space_of_RealSequences is right_complementable ::_thesis: ( Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof
let v be Element of Linear_Space_of_RealSequences; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
thus  ex w being VECTOR of Linear_Space_of_RealSequences st v + w = 0. Linear_Space_of_RealSequences by Th6; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
thus  for a being real number
for v, w being VECTOR of Linear_Space_of_RealSequences holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being VECTOR of Linear_Space_of_RealSequences holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real by XREAL_0:def_1;
 for v, w being VECTOR of Linear_Space_of_RealSequences holds a * (v + w) = (a * v) + (a * w) by Th7;
hence  for v, w being VECTOR of Linear_Space_of_RealSequences holds a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of Linear_Space_of_RealSequences holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
 for v being VECTOR of Linear_Space_of_RealSequences holds (a + b) * v = (a * v) + (b * v) by Th8;
hence  for v being VECTOR of Linear_Space_of_RealSequences holds (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
thus  for a, b being real number
for v being VECTOR of Linear_Space_of_RealSequences holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: Linear_Space_of_RealSequences is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
 for v being VECTOR of Linear_Space_of_RealSequences holds (a * b) * v = a * (b * v) by Th9;
hence  for v being VECTOR of Linear_Space_of_RealSequences holds (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of Linear_Space_of_RealSequences; :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
thus  1 * v = v by Th10; ::_thesis: verum
end;
end;

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume B1: ( X1 is linearly-closed & not X1 is empty ) ;
func Add_ (X1,X) ->  BinOp of X1 equals :Def8: :: RSSPACE:def 8
 the addF of X || X1;
correctness
coherence
the addF of X || X1 is BinOp of X1;
proof
A1: dom the addF of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1;
A2: for z being set st z in [:X1,X1:] holds
( the addF of X || X1) . z in X1
proof
let z be set ; ::_thesis: ( z in [:X1,X1:] implies ( the addF of X || X1) . z in X1 )
assume A3: z in [:X1,X1:] ; ::_thesis: ( the addF of X || X1) . z in X1
consider r, x being set  such that
A4: ( r in X1 & x in X1 ) and
A5: z = [r,x] by A3, ZFMISC_1:def_2;
reconsider y = x, r1 = r as VECTOR of X by A4;
 [r,x] in dom ( the addF of X || X1) by A1, A3, A5, RELAT_1:62, ZFMISC_1:96;
then  ( the addF of X || X1) . z = r1 + y by A5, FUNCT_1:47;
hence  ( the addF of X || X1) . z in X1 by B1, A4, RLSUB_1:def_1; ::_thesis: verum
end;
 dom ( the addF of X || X1) = [:X1,X1:] by A1, RELAT_1:62, ZFMISC_1:96;
hence  the addF of X || X1 is BinOp of X1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Add_ RSSPACE:def_8_:_
 for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Add_ (X1,X) = the addF of X || X1;

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume B1: ( X1 is linearly-closed & not X1 is empty ) ;
func Mult_ (X1,X) ->  Function of [:REAL,X1:],X1 equals :Def9: :: RSSPACE:def 9
 the Mult of X | [:REAL,X1:];
correctness
coherence
the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;
proof
A1: ( [:REAL,X1:] c= [:REAL, the carrier of X:] & dom the Mult of X = [:REAL, the carrier of X:] ) by FUNCT_2:def_1, ZFMISC_1:95;
A2: for z being set st z in [:REAL,X1:] holds
( the Mult of X | [:REAL,X1:]) . z in X1
proof
let z be set ; ::_thesis: ( z in [:REAL,X1:] implies ( the Mult of X | [:REAL,X1:]) . z in X1 )
assume A3: z in [:REAL,X1:] ; ::_thesis: ( the Mult of X | [:REAL,X1:]) . z in X1
consider r, x being set  such that
A4: r in REAL and
A5: x in X1 and
A6: z = [r,x] by A3, ZFMISC_1:def_2;
reconsider r = r as Real by A4;
reconsider y = x as VECTOR of X by A5;
 [r,x] in dom ( the Mult of X | [:REAL,X1:]) by A1, A3, A6, RELAT_1:62;
then  ( the Mult of X | [:REAL,X1:]) . z = r * y by A6, FUNCT_1:47;
hence  ( the Mult of X | [:REAL,X1:]) . z in X1 by B1, A5, RLSUB_1:def_1; ::_thesis: verum
end;
 dom ( the Mult of X | [:REAL,X1:]) = [:REAL,X1:] by A1, RELAT_1:62;
hence  the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1 by A2, FUNCT_2:3; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Mult_ RSSPACE:def_9_:_
 for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Mult_ (X1,X) = the Mult of X | [:REAL,X1:];

definition
let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is linearly-closed & not X1 is empty ) ;
func Zero_ (X1,X) ->  Element of X1 equals :Def10: :: RSSPACE:def 10
 0. X;
correctness
coherence
0. X is Element of X1;
proof
set v = the Element of X1;
 the Element of X1 in X1 by A1;
then reconsider v = the Element of X1 as Element of X ;
 v - v = 0. X by RLVECT_1:15;
hence  0. X is Element of X1 by A1, RLSUB_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines Zero_ RSSPACE:def_10_:_
 for X being RealLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Zero_ (X1,X) = 0. X;

theorem Th11: :: RSSPACE:11
for V being RealLinearSpace
for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds
RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
proof
let V be RealLinearSpace; ::_thesis: for V1 being Subset of V st V1 is linearly-closed & not V1 is empty holds
RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
let V1 be Subset of V; ::_thesis: ( V1 is linearly-closed & not V1 is empty implies RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V )
assume A1: ( V1 is linearly-closed & not V1 is empty ) ; ::_thesis: RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V
A2: Mult_ (V1,V) = the Mult of V | [:REAL,V1:] by A1, Def9;
 ( Zero_ (V1,V) = 0. V & Add_ (V1,V) = the addF of V || V1 ) by A1, Def8, Def10;
hence  RLSStruct(# V1,(Zero_ (V1,V)),(Add_ (V1,V)),(Mult_ (V1,V)) #) is Subspace of V by A1, A2, RLSUB_1:24; ::_thesis: verum
end;

definition
func the_set_of_l2RealSequences  ->  Subset of Linear_Space_of_RealSequences means :Def11: :: RSSPACE:def 11
 for x being set holds
( x in it iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) );
existence
 ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) )
proof
defpred S1[ set ] means (seq_id $1) (#) (seq_id $1) is summable ;
consider IT being set  such that
A1: for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in IT holds
x in the_set_of_RealSequences by A1;
then  IT is Subset of the_set_of_RealSequences by TARSKI:def_3;
hence  ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) holds
b1 = b2
proof
let X1, X2 be Subset of Linear_Space_of_RealSequences; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) & ( for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) and
A3: for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) ; ::_thesis: X1 = X2
thus  X1 c= X2 :: according to XBOOLE_0:def_10 ::_thesis: X2 c= X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume A4: x in X1 ; ::_thesis: x in X2
then  (seq_id x) (#) (seq_id x) is summable by A2;
hence  x in X2 by A3, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 )
assume A5: x in X2 ; ::_thesis: x in X1
then  (seq_id x) (#) (seq_id x) is summable by A3;
hence  x in X1 by A2, A5; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines the_set_of_l2RealSequences RSSPACE:def_11_:_
 for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_l2RealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) );

registration
cluster the_set_of_l2RealSequences  ->  non empty linearly-closed ;
coherence
 ( the_set_of_l2RealSequences is linearly-closed & not the_set_of_l2RealSequences is empty )
proof
set W = the_set_of_l2RealSequences ;
A1: for a being Real
for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l2RealSequences holds
a * v in the_set_of_l2RealSequences
proof
let a be Real; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l2RealSequences holds
a * v in the_set_of_l2RealSequences
let v be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_l2RealSequences implies a * v in the_set_of_l2RealSequences )
assume  v in the_set_of_l2RealSequences ; ::_thesis: a * v in the_set_of_l2RealSequences
then A2: (seq_id v) (#) (seq_id v) is summable by Def11;
seq_id (a * v) = seq_id (a (#) (seq_id v)) by Th3
.= a (#) (seq_id v) by Th1 ;
then (seq_id (a * v)) (#) (seq_id (a * v)) = a (#) ((a (#) (seq_id v)) (#) (seq_id v)) by SEQ_1:19
.= a (#) (a (#) ((seq_id v) (#) (seq_id v))) by SEQ_1:18
.= (a * a) (#) ((seq_id v) (#) (seq_id v)) by SEQ_1:23 ;
then  (seq_id (a * v)) (#) (seq_id (a * v)) is summable by A2, SERIES_1:10;
hence  a * v in the_set_of_l2RealSequences by Def11; ::_thesis: verum
end;
A3: for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l2RealSequences & u in the_set_of_l2RealSequences holds
v + u in the_set_of_l2RealSequences
proof
let v, u be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_l2RealSequences & u in the_set_of_l2RealSequences implies v + u in the_set_of_l2RealSequences )
assume that
A4: v in the_set_of_l2RealSequences and
A5: u in the_set_of_l2RealSequences ; ::_thesis: v + u in the_set_of_l2RealSequences
 (seq_id (v + u)) (#) (seq_id (v + u)) is summable
proof
set r = (seq_id (v + u)) (#) (seq_id (v + u));
set q = (seq_id u) (#) (seq_id u);
set p = (seq_id v) (#) (seq_id v);
A6: for n being Element of NAT holds 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n
 ((seq_id (v + u)) (#) (seq_id (v + u))) . n = ((seq_id (v + u)) . n) * ((seq_id (v + u)) . n) by SEQ_1:8;
hence  0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n by XREAL_1:63; ::_thesis: verum
end;
A7: for n being Element of NAT holds ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n
proof
set s = seq_id v;
set t = seq_id u;
let n be Element of NAT ; ::_thesis: ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n
reconsider sn = (seq_id v) . n, tn = (seq_id u) . n as Real ;
A8: ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n = ((2 (#) ((seq_id v) (#) (seq_id v))) . n) + ((2 (#) ((seq_id u) (#) (seq_id u))) . n) by SEQ_1:7
.= (2 * (((seq_id v) (#) (seq_id v)) . n)) + ((2 (#) ((seq_id u) (#) (seq_id u))) . n) by SEQ_1:9
.= (2 * (((seq_id v) (#) (seq_id v)) . n)) + (2 * (((seq_id u) (#) (seq_id u)) . n)) by SEQ_1:9
.= (2 * (((seq_id v) . n) * ((seq_id v) . n))) + (2 * (((seq_id u) (#) (seq_id u)) . n)) by SEQ_1:8
.= (2 * (sn ^2)) + (2 * (tn ^2)) by SEQ_1:8 ;
A9: 0 <= (sn - tn) ^2 by XREAL_1:63;
A10: seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by Def4
.= (seq_id v) + (seq_id u) by Th1 ;
((seq_id (v + u)) (#) (seq_id (v + u))) . n = ((seq_id (v + u)) . n) * ((seq_id (v + u)) . n) by SEQ_1:8
.= (((seq_id v) . n) + ((seq_id u) . n)) * (((seq_id v) + (seq_id u)) . n) by A10, SEQ_1:7
.= (((seq_id v) . n) + ((seq_id u) . n)) ^2 by SEQ_1:7
.= ((sn ^2) + ((2 * sn) * tn)) + (tn ^2) ;
then  0 + (((seq_id (v + u)) (#) (seq_id (v + u))) . n) <= ((((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n) - (((seq_id (v + u)) (#) (seq_id (v + u))) . n)) + (((seq_id (v + u)) (#) (seq_id (v + u))) . n) by A8, A9, XREAL_1:7;
hence  ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n ; ::_thesis: verum
end;
 (seq_id u) (#) (seq_id u) is summable by A5, Def11;
then A11: 2 (#) ((seq_id u) (#) (seq_id u)) is summable by SERIES_1:10;
 (seq_id v) (#) (seq_id v) is summable by A4, Def11;
then  2 (#) ((seq_id v) (#) (seq_id v)) is summable by SERIES_1:10;
then  (2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u))) is summable by A11, SERIES_1:7;
hence  (seq_id (v + u)) (#) (seq_id (v + u)) is summable by A6, A7, SERIES_1:20; ::_thesis: verum
end;
hence  v + u in the_set_of_l2RealSequences by Def11; ::_thesis: verum
end;
 (seq_id Zeroseq) (#) (seq_id Zeroseq) is absolutely_summable
proof
reconsider rseq = (seq_id Zeroseq) (#) (seq_id Zeroseq) as Real_Sequence ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_rseq_._n_=_0
let n be Element of NAT ; ::_thesis: rseq . n = 0
thus rseq . n = ((seq_id Zeroseq) . n) * ((seq_id Zeroseq) . n) by SEQ_1:8
.= ((seq_id Zeroseq) . n) * 0 by Def6
.= 0 ; ::_thesis: verum
end;
hence  (seq_id Zeroseq) (#) (seq_id Zeroseq) is absolutely_summable by COMSEQ_3:3; ::_thesis: verum
end;
hence  ( the_set_of_l2RealSequences is linearly-closed & not the_set_of_l2RealSequences is empty ) by A3, A1, Def11, RLSUB_1:def_1; ::_thesis: verum
end;
end;

theorem :: RSSPACE:12
RLSStruct(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences by Th11;

theorem Th13: :: RSSPACE:13
RLSStruct(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)) #) is RealLinearSpace by Th11;

theorem :: RSSPACE:14
( the carrier of Linear_Space_of_RealSequences = the_set_of_RealSequences & ( for x being set holds
( x is VECTOR of Linear_Space_of_RealSequences iff x is Real_Sequence ) ) & ( for u being VECTOR of Linear_Space_of_RealSequences holds u = seq_id u ) & ( for u, v being VECTOR of Linear_Space_of_RealSequences holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of Linear_Space_of_RealSequences holds r * u = r (#) (seq_id u) ) ) by Def1, Def2, Def4, Th3;

definition
func l_scalar  ->  Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL means :: RSSPACE:def 12
 for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
it . (x,y) = Sum ((seq_id x) (#) (seq_id y));
existence
 ex b1 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y))
proof
deffunc H1( set , set ) ->  Element of REAL = Sum ((seq_id $1) (#) (seq_id $2));
set X = the_set_of_l2RealSequences ;
A1: for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
H1(x,y) in REAL ;
 ex f being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
f . (x,y) = H1(x,y) from BINOP_1:sch_2(A1);
hence  ex b1 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b2 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) holds
b1 = b2
proof
set X = the_set_of_l2RealSequences ;
let scalar1, scalar2 be Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL; ::_thesis: ( ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar2 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) implies scalar1 = scalar2 )
assume that
A2: for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) and
A3: for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar2 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ; ::_thesis: scalar1 = scalar2
 for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar1 . (x,y) = scalar2 . (x,y)
proof
let x, y be set ; ::_thesis: ( x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences implies scalar1 . (x,y) = scalar2 . (x,y) )
assume A4: ( x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences ) ; ::_thesis: scalar1 . (x,y) = scalar2 . (x,y)
thus scalar1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) by A2, A4
.= scalar2 . (x,y) by A3, A4 ; ::_thesis: verum
end;
hence  scalar1 = scalar2 by BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem  defines l_scalar RSSPACE:def_12_:_
 for b1 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL holds
( b1 = l_scalar iff for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) );

registration
cluster UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) ->  non empty ;
coherence
 not UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) is empty ;
end;

definition
func l2_Space  ->  non empty UNITSTR  equals :: RSSPACE:def 13
 UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #);
coherence
 UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #) is non empty UNITSTR ;
end;

:: deftheorem  defines l2_Space RSSPACE:def_13_:_
 l2_Space = UNITSTR(# the_set_of_l2RealSequences,(Zero_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l2RealSequences,Linear_Space_of_RealSequences)),l_scalar #);

theorem Th15: :: RSSPACE:15
for l being RLSStruct st RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace
proof
let l be RLSStruct ; ::_thesis: ( RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace implies l is RealLinearSpace )
assume A1: RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace ; ::_thesis: l is RealLinearSpace
reconsider l = l as non empty RLSStruct by A1;
reconsider l0 = RLSStruct(# the carrier of l,(0. l), the addF of l, the Mult of l #) as RealLinearSpace by A1;
A2: l is Abelian
proof
let v, w be VECTOR of l; :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider v1 = v as VECTOR of l0 ;
reconsider w1 = w as VECTOR of l0 ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; ::_thesis: verum
end;
A3: l is right_zeroed
proof
let v be VECTOR of l; :: according to RLVECT_1:def_4 ::_thesis: v + (0. l) = v
reconsider v1 = v as VECTOR of l0 ;
thus v + (0. l) = v1 + (0. l0)
.= v by RLVECT_1:def_4 ; ::_thesis: verum
end;
A4: l is right_complementable
proof
let v be VECTOR of l; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider v1 = v as VECTOR of l0 ;
consider w1 being VECTOR of l0 such that
A5: v1 + w1 = 0. l0 by ALGSTR_0:def_11;
reconsider w = w1 as VECTOR of l ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. l
thus  v + w = 0. l by A5; ::_thesis: verum
end;
A6: for v being VECTOR of l holds 1 * v = v
proof
let v be VECTOR of l; ::_thesis: 1 * v = v
reconsider v1 = v as VECTOR of l0 ;
thus 1 * v = 1 * v1
.= v by RLVECT_1:def_8 ; ::_thesis: verum
end;
A7: for a, b being real number
for v being VECTOR of l holds (a * b) * v = a * (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of l holds (a * b) * v = a * (b * v)
let v be VECTOR of l; ::_thesis: (a * b) * v = a * (b * v)
reconsider v1 = v as VECTOR of l0 ;
thus (a * b) * v = (a * b) * v1
.= a * (b * v1) by RLVECT_1:def_7
.= a * (b * v) ; ::_thesis: verum
end;
A8: for a, b being real number
for v being VECTOR of l holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of l holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of l; ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider v1 = v as VECTOR of l0 ;
thus (a + b) * v = (a + b) * v1
.= (a * v1) + (b * v1) by RLVECT_1:def_6
.= (a * v) + (b * v) ; ::_thesis: verum
end;
A9: for a being real number
for v, w being VECTOR of l holds a * (v + w) = (a * v) + (a * w)
proof
let a be real number ; ::_thesis: for v, w being VECTOR of l holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of l; ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider v1 = v, w1 = w as VECTOR of l0 ;
thus a * (v + w) = a * (v1 + w1)
.= (a * v1) + (a * w1) by RLVECT_1:def_5
.= (a * v) + (a * w) ; ::_thesis: verum
end;
 l is add-associative
proof
let u, v, w be VECTOR of l; :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as VECTOR of l0 ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def_3
.= u + (v + w) ; ::_thesis: verum
end;
hence  l is RealLinearSpace by A2, A3, A4, A9, A8, A7, A6, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum
end;

theorem :: RSSPACE:16
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq is summable & Sum rseq = 0 )
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies ( rseq is summable & Sum rseq = 0 ) )
assume A1: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: ( rseq is summable & Sum rseq = 0 )
A2: for m being Element of NAT holds (Partial_Sums rseq) . m = 0
proof
defpred S1[ Nat] means rseq . $1 = (Partial_Sums rseq) . $1;
let m be Element of NAT ; ::_thesis: (Partial_Sums rseq) . m = 0
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: rseq . k = (Partial_Sums rseq) . k ; ::_thesis: S1[k + 1]
thus rseq . (k + 1) = 0 + (rseq . (k + 1))
.= (rseq . k) + (rseq . (k + 1)) by A1
.= (Partial_Sums rseq) . (k + 1) by A4, SERIES_1:def_1 ; ::_thesis: verum
end;
A5: S1[ 0 ] by SERIES_1:def_1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3);
hence (Partial_Sums rseq) . m = rseq . m
.= 0 by A1 ;
::_thesis: verum
end;
A6: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - 0) < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - 0) < p )
assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums rseq) . m) - 0) < p
take  0 ; ::_thesis: for m being Element of NAT st 0 <= m holds
abs (((Partial_Sums rseq) . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( 0 <= m implies abs (((Partial_Sums rseq) . m) - 0) < p )
assume  0 <= m ; ::_thesis: abs (((Partial_Sums rseq) . m) - 0) < p
abs (((Partial_Sums rseq) . m) - 0) = abs (0 - 0) by A2
.= 0 by ABSVALUE:def_1 ;
hence  abs (((Partial_Sums rseq) . m) - 0) < p by A7; ::_thesis: verum
end;
then A8: Partial_Sums rseq is convergent by SEQ_2:def_6;
then  lim (Partial_Sums rseq) = 0 by A6, SEQ_2:def_7;
hence  ( rseq is summable & Sum rseq = 0 ) by A8, SERIES_1:def_2, SERIES_1:def_3; ::_thesis: verum
end;

theorem :: RSSPACE:17
for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 holds
for n being Element of NAT holds rseq . n = 0
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 implies for n being Element of NAT holds rseq . n = 0 )
assume that
A1: for n being Element of NAT holds 0 <= rseq . n and
A2: rseq is summable and
A3: Sum rseq = 0 ; ::_thesis: for n being Element of NAT holds rseq . n = 0
A4: Partial_Sums rseq is bounded_above by A1, A2, SERIES_1:17;
A5: for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq
proof
let n be Nat; ::_thesis: (Partial_Sums rseq) . n <= Sum rseq
 n in NAT by ORDINAL1:def_12;
then  (Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A4, SEQ_4:37, SERIES_1:16;
hence  (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def_3; ::_thesis: verum
end;
A6: Partial_Sums rseq is V46() by A1, SERIES_1:16;
now__::_thesis:_for_n1_being_Element_of_NAT_holds_not_rseq_._n1_<>_0
given n1 being Element of NAT  such that A7: rseq . n1 <> 0 ; ::_thesis: contradiction
A8: for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (Partial_Sums rseq) . n
A9: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def_1;
 0 <= rseq . 0 by A1;
hence  0 <= (Partial_Sums rseq) . n by A6, A9, SEQM_3:5; ::_thesis: verum
end;
 (Partial_Sums rseq) . n1 > 0
proof
now__::_thesis:_(_(_n1_=_0_&_(Partial_Sums_rseq)_._n1_>_0_)_or_(_n1_<>_0_&_(Partial_Sums_rseq)_._n1_>_0_)_)
percases ( n1 = 0 or n1 <> 0 ) ;
caseA10: n1 = 0 ; ::_thesis: (Partial_Sums rseq) . n1 > 0
then  (Partial_Sums rseq) . n1 = rseq . 0 by SERIES_1:def_1;
hence  (Partial_Sums rseq) . n1 > 0 by A1, A7, A10; ::_thesis: verum
end;
caseA11: n1 <> 0 ; ::_thesis: (Partial_Sums rseq) . n1 > 0
set nn = n1 - 1;
A12: ( (n1 - 1) + 1 = n1 & 0 <= rseq . n1 ) by A1;
 0 <= n1 by NAT_1:2;
then  0 + 1 <= n1 by A11, INT_1:7;
then A13: n1 - 1 in NAT by INT_1:5;
then  0 <= (Partial_Sums rseq) . (n1 - 1) by A8;
then  (rseq . n1) + 0 <= (rseq . n1) + ((Partial_Sums rseq) . (n1 - 1)) by XREAL_1:7;
hence  (Partial_Sums rseq) . n1 > 0 by A7, A13, A12, SERIES_1:def_1; ::_thesis: verum
end;
end;
end;
hence  (Partial_Sums rseq) . n1 > 0 ; ::_thesis: verum
end;
hence  contradiction by A3, A5; ::_thesis: verum
end;
hence  for n being Element of NAT holds rseq . n = 0 ; ::_thesis: verum
end;

registration
cluster l2_Space  ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( l2_Space is Abelian & l2_Space is add-associative & l2_Space is right_zeroed & l2_Space is right_complementable & l2_Space is vector-distributive & l2_Space is scalar-distributive & l2_Space is scalar-associative & l2_Space is scalar-unital ) by Th13, Th15;
end;