:: RSSPACE semantic presentation

definition
func the_set_of_RealSequences -> non empty set means :Def1: :: RSSPACE:def 1
for b1 being set holds
( b1 in a1 iff b1 is Real_Sequence );
existence
ex b1 being non empty set st
for b2 being set holds
( b2 in b1 iff b2 is Real_Sequence )
proof end;
uniqueness
for b1, b2 being non empty set st ( for b3 being set holds
( b3 in b1 iff b3 is Real_Sequence ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is Real_Sequence ) ) holds
b1 = b2
proof 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 b2 being set holds
( b2 in b1 iff b2 is Real_Sequence ) );

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

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
for b1 being set st b1 in the_set_of_RealSequences holds
seq_id b1 = b1;

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

:: deftheorem Def3 defines R_id RSSPACE:def 3 :
for b1 being set st b1 in REAL holds
R_id b1 = b1;

theorem Th1: :: RSSPACE:1
ex b1 being BinOp of the_set_of_RealSequences st
( ( for b2, b3 being Element of the_set_of_RealSequences holds b1 . b2,b3 = (seq_id b2) + (seq_id b3) ) & b1 is commutative & b1 is associative )
proof end;

theorem Th2: :: RSSPACE:2
ex b1 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st
for b2, b3 being set st b2 in REAL & b3 in the_set_of_RealSequences holds
b1 . [b2,b3] = (R_id b2) (#) (seq_id b3)
proof end;

definition
func l_add -> BinOp of the_set_of_RealSequences means :Def4: :: RSSPACE:def 4
for b1, b2 being Element of the_set_of_RealSequences holds a1 . b1,b2 = (seq_id b1) + (seq_id b2);
existence
ex b1 being BinOp of the_set_of_RealSequences st
for b2, b3 being Element of the_set_of_RealSequences holds b1 . b2,b3 = (seq_id b2) + (seq_id b3) by Th1;
uniqueness
for b1, b2 being BinOp of the_set_of_RealSequences st ( for b3, b4 being Element of the_set_of_RealSequences holds b1 . b3,b4 = (seq_id b3) + (seq_id b4) ) & ( for b3, b4 being Element of the_set_of_RealSequences holds b2 . b3,b4 = (seq_id b3) + (seq_id b4) ) holds
b1 = b2
proof 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 b2, b3 being Element of the_set_of_RealSequences holds b1 . b2,b3 = (seq_id b2) + (seq_id b3) );

definition
func l_mult -> Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences means :Def5: :: RSSPACE:def 5
for b1, b2 being set st b1 in REAL & b2 in the_set_of_RealSequences holds
a1 . [b1,b2] = (R_id b1) (#) (seq_id b2);
existence
ex b1 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st
for b2, b3 being set st b2 in REAL & b3 in the_set_of_RealSequences holds
b1 . [b2,b3] = (R_id b2) (#) (seq_id b3) by Th2;
uniqueness
for b1, b2 being Function of [:REAL ,the_set_of_RealSequences :], the_set_of_RealSequences st ( for b3, b4 being set st b3 in REAL & b4 in the_set_of_RealSequences holds
b1 . [b3,b4] = (R_id b3) (#) (seq_id b4) ) & ( for b3, b4 being set st b3 in REAL & b4 in the_set_of_RealSequences holds
b2 . [b3,b4] = (R_id b3) (#) (seq_id b4) ) holds
b1 = b2
proof 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 b2, b3 being set st b2 in REAL & b3 in the_set_of_RealSequences holds
b1 . [b2,b3] = (R_id b2) (#) (seq_id b3) );

definition
func Zeroseq -> Element of the_set_of_RealSequences means :Def6: :: RSSPACE:def 6
for b1 being Nat holds (seq_id a1) . b1 = 0;
existence
ex b1 being Element of the_set_of_RealSequences st
for b2 being Nat holds (seq_id b1) . b2 = 0
proof end;
uniqueness
for b1, b2 being Element of the_set_of_RealSequences st ( for b3 being Nat holds (seq_id b1) . b3 = 0 ) & ( for b3 being Nat holds (seq_id b2) . b3 = 0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :
for b1 being Element of the_set_of_RealSequences holds
( b1 = Zeroseq iff for b2 being Nat holds (seq_id b1) . b2 = 0 );

theorem Th3: :: RSSPACE:3
for b1 being Real_Sequence holds seq_id b1 = b1
proof end;

theorem Th4: :: RSSPACE:4
for b1, b2 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds b1 + b2 = (seq_id b1) + (seq_id b2)
proof end;

theorem Th5: :: RSSPACE:5
for b1 being Real
for b2 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds b1 * b2 = b1 (#) (seq_id b2)
proof 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 end;
end;

Lemma12: for b1, b2 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds b1 + b2 = b2 + b1
;

theorem Th6: :: RSSPACE:6
for b1, b2, b3 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds (b1 + b2) + b3 = b1 + (b2 + b3)
proof end;

theorem Th7: :: RSSPACE:7
for b1 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds b1 + (0. RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #)) = b1
proof end;

theorem Th8: :: RSSPACE:8
for b1 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) ex b2 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) st b1 + b2 = 0. RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #)
proof end;

theorem Th9: :: RSSPACE:9
for b1 being Real
for b2, b3 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds b1 * (b2 + b3) = (b1 * b2) + (b1 * b3)
proof end;

theorem Th10: :: RSSPACE:10
for b1, b2 being Real
for b3 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3)
proof end;

theorem Th11: :: RSSPACE:11
for b1, b2 being Real
for b3 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds (b1 * b2) * b3 = b1 * (b2 * b3)
proof end;

theorem Th12: :: RSSPACE:12
for b1 being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds 1 * b1 = b1
proof end;

definition
func Linear_Space_of_RealSequences -> RealLinearSpace 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 RealLinearSpace;
by Lemma12, Th6, Th7, Th8, Th9, Th10, Th11, Th12, RLVECT_1:7;
end;

:: deftheorem Def7 defines Linear_Space_of_RealSequences RSSPACE:def 7 :
Linear_Space_of_RealSequences = RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #);

definition
let c1 be RealLinearSpace;
let c2 be Subset of c1;
assume E20: ( c2 is lineary-closed & not c2 is empty ) ;
func Add_ c2,c1 -> BinOp of a2 equals :Def8: :: RSSPACE:def 8
the add of a1 || a2;
correctness
coherence
the add of c1 || c2 is BinOp of c2;
proof end;
end;

:: deftheorem Def8 defines Add_ RSSPACE:def 8 :
for b1 being RealLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
Add_ b2,b1 = the add of b1 || b2;

definition
let c1 be RealLinearSpace;
let c2 be Subset of c1;
assume E21: ( c2 is lineary-closed & not c2 is empty ) ;
func Mult_ c2,c1 -> Function of [:REAL ,a2:],a2 equals :Def9: :: RSSPACE:def 9
the Mult of a1 | [:REAL ,a2:];
correctness
coherence
the Mult of c1 | [:REAL ,c2:] is Function of [:REAL ,c2:],c2;
proof end;
end;

:: deftheorem Def9 defines Mult_ RSSPACE:def 9 :
for b1 being RealLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
Mult_ b2,b1 = the Mult of b1 | [:REAL ,b2:];

definition
let c1 be RealLinearSpace;
let c2 be Subset of c1;
assume E22: ( c2 is lineary-closed & not c2 is empty ) ;
func Zero_ c2,c1 -> Element of a2 equals :Def10: :: RSSPACE:def 10
 0. a1;
correctness
coherence
0. c1 is Element of c2;
proof end;
end;

:: deftheorem Def10 defines Zero_ RSSPACE:def 10 :
for b1 being RealLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
Zero_ b2,b1 = 0. b1;

theorem Th13: :: RSSPACE:13
for b1 being RealLinearSpace
for b2 being Subset of b1 st b2 is lineary-closed & not b2 is empty holds
RLSStruct(# b2,(Zero_ b2,b1),(Add_ b2,b1),(Mult_ b2,b1) #) is Subspace of b1
proof end;

definition
func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences means :Def11: :: RSSPACE:def 11
for b1 being set holds
( b1 in a1 iff ( b1 in the_set_of_RealSequences & (seq_id b1) (#) (seq_id b1) is summable ) );
existence
ex b1 being Subset of Linear_Space_of_RealSequences st
for b2 being set holds
( b2 in b1 iff ( b2 in the_set_of_RealSequences & (seq_id b2) (#) (seq_id b2) is summable ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for b3 being set holds
( b3 in b1 iff ( b3 in the_set_of_RealSequences & (seq_id b3) (#) (seq_id b3) is summable ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 in the_set_of_RealSequences & (seq_id b3) (#) (seq_id b3) is summable ) ) ) holds
b1 = b2
proof 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 b2 being set holds
( b2 in b1 iff ( b2 in the_set_of_RealSequences & (seq_id b2) (#) (seq_id b2) is summable ) ) );

registration
cluster the_set_of_l2RealSequences -> non empty lineary-closed ;
coherence
( the_set_of_l2RealSequences is lineary-closed & not the_set_of_l2RealSequences is empty )
proof end;
end;

theorem Th14: :: RSSPACE:14
canceled;

theorem Th15: :: RSSPACE:15
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 Th13;

theorem Th16: :: RSSPACE:16
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 Th13;

theorem Th17: :: RSSPACE:17
( the carrier of Linear_Space_of_RealSequences = the_set_of_RealSequences & ( for b1 being set holds
( b1 is VECTOR of Linear_Space_of_RealSequences iff b1 is Real_Sequence ) ) & ( for b1 being VECTOR of Linear_Space_of_RealSequences holds b1 = seq_id b1 ) & ( for b1, b2 being VECTOR of Linear_Space_of_RealSequences holds b1 + b2 = (seq_id b1) + (seq_id b2) ) & ( for b1 being Real
for b2 being VECTOR of Linear_Space_of_RealSequences holds b1 * b2 = b1 (#) (seq_id b2) ) ) by Def1, Def2, Th4, Th5;

theorem Th18: :: RSSPACE:18
ex b1 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st
for b2, b3 being set st b2 in the_set_of_l2RealSequences & b3 in the_set_of_l2RealSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) (seq_id b3))
proof end;

definition
func l_scalar -> Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL means :: RSSPACE:def 12
for b1, b2 being set st b1 in the_set_of_l2RealSequences & b2 in the_set_of_l2RealSequences holds
a1 . [b1,b2] = Sum ((seq_id b1) (#) (seq_id b2));
existence
ex b1 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st
for b2, b3 being set st b2 in the_set_of_l2RealSequences & b3 in the_set_of_l2RealSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) (seq_id b3)) by Th18;
uniqueness
for b1, b2 being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :], REAL st ( for b3, b4 being set st b3 in the_set_of_l2RealSequences & b4 in the_set_of_l2RealSequences holds
b1 . [b3,b4] = Sum ((seq_id b3) (#) (seq_id b4)) ) & ( for b3, b4 being set st b3 in the_set_of_l2RealSequences & b4 in the_set_of_l2RealSequences holds
b2 . [b3,b4] = Sum ((seq_id b3) (#) (seq_id b4)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 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 b2, b3 being set st b2 in the_set_of_l2RealSequences & b3 in the_set_of_l2RealSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) (seq_id b3)) );

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 Def13 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 Th19: :: RSSPACE:19
for b1 being UNITSTR st RLSStruct(# the carrier of b1,the Zero of b1,the add of b1,the Mult of b1 #) is RealLinearSpace holds
b1 is RealLinearSpace
proof end;

theorem Th20: :: RSSPACE:20
for b1 being Real_Sequence st ( for b2 being Nat holds b1 . b2 = 0 ) holds
( b1 is summable & Sum b1 = 0 )
proof end;

theorem Th21: :: RSSPACE:21
for b1 being Real_Sequence st ( for b2 being Nat holds 0 <= b1 . b2 ) & b1 is summable & Sum b1 = 0 holds
for b2 being Nat holds b1 . b2 = 0
proof end;

registration
cluster l2_Space -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence
( l2_Space is Abelian & l2_Space is add-associative & l2_Space is right_zeroed & l2_Space is right_complementable & l2_Space is RealLinearSpace-like ) by Th16, Th19;
end;