:: RSSPACE2 semantic presentation

theorem Th1: :: RSSPACE2:1
( the carrier of l2_Space = the_set_of_l2RealSequences & ( for b1 being set holds
( b1 is VECTOR of l2_Space iff ( b1 is Real_Sequence & (seq_id b1) (#) (seq_id b1) is summable ) ) ) & 0. l2_Space = Zeroseq & ( for b1 being VECTOR of l2_Space holds b1 = seq_id b1 ) & ( for b1, b2 being VECTOR of l2_Space holds b1 + b2 = (seq_id b1) + (seq_id b2) ) & ( for b1 being Real
for b2 being VECTOR of l2_Space holds b1 * b2 = b1 (#) (seq_id b2) ) & ( for b1 being VECTOR of l2_Space holds
( - b1 = - (seq_id b1) & seq_id (- b1) = - (seq_id b1) ) ) & ( for b1, b2 being VECTOR of l2_Space holds b1 - b2 = (seq_id b1) - (seq_id b2) ) & ( for b1, b2 being VECTOR of l2_Space holds
( (seq_id b1) (#) (seq_id b2) is summable & ( for b3, b4 being VECTOR of l2_Space holds b3 .|. b4 = Sum ((seq_id b3) (#) (seq_id b4)) ) ) ) )
proof end;

theorem Th2: :: RSSPACE2:2
for b1, b2, b3 being Point of l2_Space
for b4 being Real holds
( ( b1 .|. b1 = 0 implies b1 = 0. l2_Space ) & ( b1 = 0. l2_Space implies b1 .|. b1 = 0 ) & 0 <= b1 .|. b1 & b1 .|. b2 = b2 .|. b1 & (b1 + b2) .|. b3 = (b1 .|. b3) + (b2 .|. b3) & (b4 * b1) .|. b2 = b4 * (b1 .|. b2) )
proof end;

registration
cluster l2_Space -> RealUnitarySpace-like ;
coherence
l2_Space is RealUnitarySpace-like by Th2, BHSP_1:def 2;
end;

Lemma3: for b1 being Real_Sequence st ( for b2 being Nat holds 0 <= b1 . b2 ) holds
( ( for b2 being Nat holds 0 <= (Partial_Sums b1) . b2 ) & ( for b2 being Nat holds b1 . b2 <= (Partial_Sums b1) . b2 ) & ( b1 is summable implies ( ( for b2 being Nat holds (Partial_Sums b1) . b2 <= Sum b1 ) & ( for b2 being Nat holds b1 . b2 <= Sum b1 ) ) ) )
proof end;

Lemma4: ( ( for b1, b2 being Real holds (b1 + b2) * (b1 + b2) <= ((2 * b1) * b1) + ((2 * b2) * b2) ) & ( for b1, b2 being Real holds b1 * b1 <= ((2 * (b1 - b2)) * (b1 - b2)) + ((2 * b2) * b2) ) )
proof end;

Lemma5: for b1 being Real
for b2 being Real_Sequence st b2 is convergent & ex b3 being Nat st
for b4 being Nat st b3 <= b4 holds
b2 . b4 <= b1 holds
lim b2 <= b1
proof end;

Lemma6: for b1 being Real
for b2 being Real_Sequence st b2 is convergent holds
for b3 being Real_Sequence st ( for b4 being Nat holds b3 . b4 = ((b2 . b4) - b1) * ((b2 . b4) - b1) ) holds
( b3 is convergent & lim b3 = ((lim b2) - b1) * ((lim b2) - b1) )
proof end;

Lemma7: for b1 being Real
for b2, b3 being Real_Sequence st b2 is convergent & b3 is convergent holds
for b4 being Real_Sequence st ( for b5 being Nat holds b4 . b5 = (((b2 . b5) - b1) * ((b2 . b5) - b1)) + (b3 . b5) ) holds
( b4 is convergent & lim b4 = (((lim b2) - b1) * ((lim b2) - b1)) + (lim b3) )
proof end;

theorem Th3: :: RSSPACE2:3
for b1 being sequence of l2_Space st b1 is_Cauchy_sequence holds
b1 is convergent
proof end;

then Lemma8: l2_Space is complete
by BHSP_3:def 6;

registration
cluster l2_Space -> RealUnitarySpace-like complete Hilbert ;
coherence
( l2_Space is Hilbert & l2_Space is complete ) by Lemma8, BHSP_3:def 7;
end;

theorem Th4: :: RSSPACE2:4
for b1 being Real_Sequence st ( for b2 being Nat holds 0 <= b1 . b2 ) holds
( ( for b2 being Nat holds 0 <= (Partial_Sums b1) . b2 ) & ( for b2 being Nat holds b1 . b2 <= (Partial_Sums b1) . b2 ) & ( b1 is summable implies ( ( for b2 being Nat holds (Partial_Sums b1) . b2 <= Sum b1 ) & ( for b2 being Nat holds b1 . b2 <= Sum b1 ) ) ) ) by Lemma3;

theorem Th5: :: RSSPACE2:5
( ( for b1, b2 being Real holds (b1 + b2) * (b1 + b2) <= ((2 * b1) * b1) + ((2 * b2) * b2) ) & ( for b1, b2 being Real holds b1 * b1 <= ((2 * (b1 - b2)) * (b1 - b2)) + ((2 * b2) * b2) ) ) by Lemma4;

theorem Th6: :: RSSPACE2:6
for b1 being Real
for b2 being Real_Sequence st b2 is convergent & ex b3 being Nat st
for b4 being Nat st b3 <= b4 holds
b2 . b4 <= b1 holds
lim b2 <= b1 by Lemma5;

theorem Th7: :: RSSPACE2:7
for b1 being Real
for b2 being Real_Sequence st b2 is convergent holds
for b3 being Real_Sequence st ( for b4 being Nat holds b3 . b4 = ((b2 . b4) - b1) * ((b2 . b4) - b1) ) holds
( b3 is convergent & lim b3 = ((lim b2) - b1) * ((lim b2) - b1) ) by Lemma6;

theorem Th8: :: RSSPACE2:8
for b1 being Real
for b2, b3 being Real_Sequence st b2 is convergent & b3 is convergent holds
for b4 being Real_Sequence st ( for b5 being Nat holds b4 . b5 = (((b2 . b5) - b1) * ((b2 . b5) - b1)) + (b3 . b5) ) holds
( b4 is convergent & lim b4 = (((lim b2) - b1) * ((lim b2) - b1)) + (lim b3) ) by Lemma7;