set W = the_set_of_l2RealSequences ;
hereby :: according to RLSUB_1:def 1 :: thesis: ( ( for b1 being object
for b2 being Element of the carrier of Linear_Space_of_RealSequences holds
( not b2 in the_set_of_l2RealSequences or b1 * b2 in the_set_of_l2RealSequences ) ) & not the_set_of_l2RealSequences is empty )
let v, u be VECTOR of Linear_Space_of_RealSequences; :: thesis:
assume that
A4: v in the_set_of_l2RealSequences and
A5: u in the_set_of_l2RealSequences ; :: thesis:
(seq_id (v + u)) (#) (seq_id (v + u)) is summable
proof
set r = (seq_id (v + u)) (#) (seq_id (v + u));
set q = () (#) ();
set p = () (#) ();
A6: for n being Nat holds 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n
proof
let n be 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 Nat holds ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) (() (#) ())) + (2 (#) (() (#) ()))) . n
proof
set s = seq_id v;
set t = seq_id u;
let n be Nat; :: thesis: ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) (() (#) ())) + (2 (#) (() (#) ()))) . n
reconsider sn = () . n, tn = () . n as Real ;
A8: ((2 (#) (() (#) ())) + (2 (#) (() (#) ()))) . n = ((2 (#) (() (#) ())) . n) + ((2 (#) (() (#) ())) . n) by SEQ_1:7
.= (2 * ((() (#) ()) . n)) + ((2 (#) (() (#) ())) . n) by SEQ_1:9
.= (2 * ((() (#) ()) . n)) + (2 * ((() (#) ()) . n)) by SEQ_1:9
.= (2 * ((() . n) * (() . n))) + (2 * ((() (#) ()) . n)) by SEQ_1:8
.= (2 * (sn ^2)) + (2 * (tn ^2)) by SEQ_1:8 ;
A9: 0 <= (sn - tn) ^2 by XREAL_1:63;
reconsider vu = v + u as Element of Funcs (NAT,REAL) ;
n in NAT by ORDINAL1:def 12;
then vu . n = (() . n) + (() . n) by FUNCSDOM:1;
then ((seq_id (v + u)) (#) (seq_id (v + u))) . n = ((() . n) + (() . n)) ^2 by SEQ_1:8
.= ((sn ^2) + ((2 * sn) * tn)) + (tn ^2) ;
then 0 + (((seq_id (v + u)) (#) (seq_id (v + u))) . n) <= ((((2 (#) (() (#) ())) + (2 (#) (() (#) ()))) . n) - (((seq_id (v + u)) (#) (seq_id (v + u))) . n)) + (((seq_id (v + u)) (#) (seq_id (v + u))) . n) by ;
hence ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) (() (#) ())) + (2 (#) (() (#) ()))) . n ; :: thesis: verum
end;
(seq_id u) (#) () is summable by ;
then A10: 2 (#) (() (#) ()) is summable by SERIES_1:10;
(seq_id v) (#) () is summable by ;
then 2 (#) (() (#) ()) is summable by SERIES_1:10;
then (2 (#) (() (#) ())) + (2 (#) (() (#) ())) is summable by ;
hence (seq_id (v + u)) (#) (seq_id (v + u)) is summable by ; :: thesis: verum
end;
hence v + u in the_set_of_l2RealSequences by Def8; :: thesis: verum
end;
hereby :: thesis:
let a be Real; :: thesis:
let v be VECTOR of Linear_Space_of_RealSequences; :: thesis:
assume v in the_set_of_l2RealSequences ; :: thesis:
then A2: (seq_id v) (#) () is summable by Def8;
a * v = a (#) () by Th3;
then (seq_id (a * v)) (#) (seq_id (a * v)) = a (#) ((a (#) ()) (#) ()) by SEQ_1:19
.= a (#) (a (#) (() (#) ())) by SEQ_1:18
.= (a * a) (#) (() (#) ()) by SEQ_1:23 ;
then (seq_id (a * v)) (#) (seq_id (a * v)) is summable by ;
hence a * v in the_set_of_l2RealSequences by Def8; :: thesis: verum
end;
(seq_id Zeroseq) (#) is absolutely_summable
proof
reconsider rseq = (#) as Real_Sequence ;
now :: thesis: for n being Nat holds rseq . n = 0
let n be Nat; :: thesis: rseq . n = 0
thus rseq . n = ( . n) * ( . n) by SEQ_1:8
.= ( . n) * 0 by
.= 0 ; :: thesis: verum
end;
hence (seq_id Zeroseq) (#) is absolutely_summable by COMSEQ_3:3; :: thesis: verum
end;
hence not the_set_of_l2RealSequences is empty by Def8; :: thesis: verum