:: RSSPACE semantic presentation

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def 1 :

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 by A1, Def1;

end;

:: deftheorem Def2 defines seq_id RSSPACE:def 2 :

definition

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

end;

:: deftheorem Def3 defines R_id RSSPACE:def 3 :

theorem Th1: :: RSSPACE:1

ex ADD being BinOp of the_set_of_RealSequences st
( ( for a, b being Element of the_set_of_RealSequences holds ADD . a,b = (seq_id a) + (seq_id b) ) & ADD is commutative & ADD is associative )

proof end;

theorem Th2: :: RSSPACE:2

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] = (R_id r) (#) (seq_id x)

proof end;

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 by Th1;
uniqueness

proof end;

end;

:: deftheorem Def4 defines l_add RSSPACE:def 4 :

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 by Th2;
uniqueness

proof end;

end;

:: deftheorem Def5 defines l_mult RSSPACE:def 5 :

definition

func Zeroseq -> Element of the_set_of_RealSequences means :Def6: :: RSSPACE:def 6
for n being Nat holds (seq_id it) . n = 0;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :

theorem Th3: :: RSSPACE:3

for x being Real_Sequence holds seq_id x = x

proof end;

theorem Th4: :: RSSPACE:4

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)

proof end;

theorem Th5: :: RSSPACE:5

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 end;

registration

cluster RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) -> Abelian ;
coherence

proof end;

end;

Lm1: for u, v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds u + v = v + u
;

theorem Th6: :: RSSPACE:6

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 end;

theorem Th7: :: RSSPACE:7

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 end;

theorem Th8: :: RSSPACE:8

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 end;

theorem Th9: :: RSSPACE:9

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 end;

theorem Th10: :: RSSPACE:10

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 end;

theorem Th11: :: RSSPACE:11

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 end;

theorem Th12: :: RSSPACE:12

for v being VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #) holds 1 * v = v

proof end;

definition

func Linear_Space_of_RealSequences -> RealLinearSpace equals :: RSSPACE:def 7
RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #);
correctness by Lm1, Th6, Th7, Th8, Th9, Th10, Th11, Th12, RLVECT_1:7;

end;

:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :

definition

let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Add_ X1,X -> BinOp of X1 equals :Def8: :: RSSPACE:def 8
the add of X || X1;
correctness

proof end;

end;

:: deftheorem Def8 defines Add_ RSSPACE:def 8 :

definition

let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-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

proof end;

end;

:: deftheorem Def9 defines Mult_ RSSPACE:def 9 :

definition

let X be RealLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Zero_ X1,X -> Element of X1 equals :Def10: :: RSSPACE:def 10
0. X;
correctness

proof end;

end;

:: deftheorem Def10 defines Zero_ RSSPACE:def 10 :

theorem Th13: :: RSSPACE:13

for V being RealLinearSpace
for V1 being Subset of V st V1 is lineary-closed & not V1 is empty holds
RLSStruct(# V1,(Zero_ V1,V),(Add_ V1,V),(Mult_ V1,V) #) is Subspace of V

proof end;

definition