begin
:: deftheorem Def1 defines the_set_of_RealSequences RSSPACE:def 1 :
:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
:: deftheorem Def3 defines R_id RSSPACE:def 3 :
theorem Th1:
theorem Th2:
:: 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:
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)
by Th2;
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
end;
:: deftheorem Def5 defines l_mult RSSPACE:def 5 :
:: deftheorem Def6 defines Zeroseq RSSPACE:def 6 :
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines Linear_Space_of_RealSequences RSSPACE:def 7 :
:: deftheorem Def8 defines Add_ RSSPACE:def 8 :
:: deftheorem Def9 defines Mult_ RSSPACE:def 9 :
:: deftheorem Def10 defines Zero_ RSSPACE:def 10 :
theorem Th13:
:: deftheorem Def11 defines the_set_of_l2RealSequences RSSPACE:def 11 :
theorem
canceled;
theorem
theorem Th16:
theorem
theorem Th18:
definition
func l_scalar -> Function of
[:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :],
REAL means
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))
by Th18;
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
end;
:: deftheorem defines l_scalar RSSPACE:def 12 :
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
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 :
theorem Th19:
theorem
theorem