:: BHSP_4 semantic presentation

deffunc H1( RealUnitarySpace) -> Element of the carrier of a1 = 0. a1;

scheme :: BHSP_4:sch 1
s1{ F1() -> non empty RLSStruct , F2() -> Point of F1(), F3( Nat, Point of F1()) -> Point of F1() } :
ex b1 being Function of NAT ,the carrier of F1() st
( b1 . 0 = F2() & ( for b2 being Element of NAT
for b3 being Point of F1() holds
( b3 = b1 . b2 implies b1 . (b2 + 1) = F3(b2,b3) ) ) )
provided
proof
consider c1 being Function of NAT ,the carrier of F1() such that
E1: ( c1 . 0 = F2() & ( for b1 being Element of NAT holds c1 . (b1 + 1) = F3(b1,(c1 . b1)) ) ) from RECDEF_1:sch 4();
 take c1 ;
thus c1 . 0 = F2() by E1;
thus for b1 being Nat
for b2 being Point of F1() holds
( b2 = c1 . b1 implies c1 . (b1 + 1) = F3(b1,b2) ) by E1;
end;

definition
let c1 be non empty RLSStruct ;
let c2 be sequence of c1;
func Partial_Sums c2 -> sequence of a1 means :E1: :: BHSP_4:def 1
( a3 . 0 = a2 . 0 & ( for b1 being Nat holds a3 . (b1 + 1) = (a3 . b1) + (a2 . (b1 + 1)) ) );
existence
ex b1 being sequence of c1 st
( b1 . 0 = c2 . 0 & ( for b2 being Nat holds b1 . (b2 + 1) = (b1 . b2) + (c2 . (b2 + 1)) ) )
proof
deffunc H2( Nat, Point of c1) -> Element of the carrier of c1 = a2 + (c2 . (a1 + 1));
consider c3 being Function of NAT ,the carrier of c1 such that
E1: ( c3 . 0 = c2 . 0 & ( for b1 being Nat
for b2 being Point of c1 holds
( b2 = c3 . b1 implies c3 . (b1 + 1) = H2(b1,b2) ) ) ) from BHSP_4:sch 1();
 take c3 ;
thus ( c3 . 0 = c2 . 0 & ( for b1 being Nat holds c3 . (b1 + 1) = (c3 . b1) + (c2 . (b1 + 1)) ) ) by E1;
end;
uniqueness
for b1, b2 being sequence of c1 holds
( ( b1 . 0 = c2 . 0 & ( for b3 being Nat holds b1 . (b3 + 1) = (b1 . b3) + (c2 . (b3 + 1)) ) & b2 . 0 = c2 . 0 & ( for b3 being Nat holds b2 . (b3 + 1) = (b2 . b3) + (c2 . (b3 + 1)) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be sequence of c1;
assume that
E1: ( c3 . 0 = c2 . 0 & ( for b1 being Nat holds c3 . (b1 + 1) = (c3 . b1) + (c2 . (b1 + 1)) ) ) and
E2: ( c4 . 0 = c2 . 0 & ( for b1 being Nat holds c4 . (b1 + 1) = (c4 . b1) + (c2 . (b1 + 1)) ) ) ;
defpred S1[ Nat] means c3 . a1 = c4 . a1;
E3: S1[0] by E1, E2;
E4: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c5 be Nat;
assume c3 . c5 = c4 . c5 ;
hence c3 . (c5 + 1) = (c4 . c5) + (c2 . (c5 + 1)) by E1
.= c4 . (c5 + 1) by E2 ;

end;
for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E3, E4);
 hence c3 = c4 by FUNCT_2:113;
end;
end;

:: deftheorem E1 defines Partial_Sums BHSP_4:def 1 :
for b1 being non empty RLSStruct
for b2, b3 being sequence of b1 holds
( b3 = Partial_Sums b2 iff ( b3 . 0 = b2 . 0 & ( for b4 being Nat holds b3 . (b4 + 1) = (b3 . b4) + (b2 . (b4 + 1)) ) ) );

theorem E2: :: BHSP_4:1
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds (Partial_Sums b2) + (Partial_Sums b3) = Partial_Sums (b2 + b3)
proof
let c1 be RealUnitarySpace;
let c2, c3 be sequence of c1;
set c4 = Partial_Sums c2;
set c5 = Partial_Sums c3;
E3: ((Partial_Sums c2) + (Partial_Sums c3)) . 0 = ((Partial_Sums c2) . 0) + ((Partial_Sums c3) . 0) by NORMSP_1:def 5
.= (c2 . 0) + ((Partial_Sums c3) . 0) by E1
.= (c2 . 0) + (c3 . 0) by E1
.= (c2 + c3) . 0 by NORMSP_1:def 5 ;
now
let c6 be Nat;
thus ((Partial_Sums c2) + (Partial_Sums c3)) . (c6 + 1) = ((Partial_Sums c2) . (c6 + 1)) + ((Partial_Sums c3) . (c6 + 1)) by NORMSP_1:def 5
.= (((Partial_Sums c2) . c6) + (c2 . (c6 + 1))) + ((Partial_Sums c3) . (c6 + 1)) by E1
.= (((Partial_Sums c2) . c6) + (c2 . (c6 + 1))) + ((c3 . (c6 + 1)) + ((Partial_Sums c3) . c6)) by E1
.= ((((Partial_Sums c2) . c6) + (c2 . (c6 + 1))) + (c3 . (c6 + 1))) + ((Partial_Sums c3) . c6) by RLVECT_1:def 6
.= (((Partial_Sums c2) . c6) + ((c2 . (c6 + 1)) + (c3 . (c6 + 1)))) + ((Partial_Sums c3) . c6) by RLVECT_1:def 6
.= (((Partial_Sums c2) . c6) + ((c2 + c3) . (c6 + 1))) + ((Partial_Sums c3) . c6) by NORMSP_1:def 5
.= (((Partial_Sums c2) . c6) + ((Partial_Sums c3) . c6)) + ((c2 + c3) . (c6 + 1)) by RLVECT_1:def 6
.= (((Partial_Sums c2) + (Partial_Sums c3)) . c6) + ((c2 + c3) . (c6 + 1)) by NORMSP_1:def 5 ;
end;
hence (Partial_Sums c2) + (Partial_Sums c3) = Partial_Sums (c2 + c3) by E3, E1;
end;

theorem E3: :: BHSP_4:2
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds (Partial_Sums b2) - (Partial_Sums b3) = Partial_Sums (b2 - b3)
proof
let c1 be RealUnitarySpace;
let c2, c3 be sequence of c1;
set c4 = Partial_Sums c2;
set c5 = Partial_Sums c3;
E4: ((Partial_Sums c2) - (Partial_Sums c3)) . 0 = ((Partial_Sums c2) . 0) - ((Partial_Sums c3) . 0) by NORMSP_1:def 6
.= (c2 . 0) - ((Partial_Sums c3) . 0) by E1
.= (c2 . 0) - (c3 . 0) by E1
.= (c2 - c3) . 0 by NORMSP_1:def 6 ;
now
let c6 be Nat;
thus ((Partial_Sums c2) - (Partial_Sums c3)) . (c6 + 1) = ((Partial_Sums c2) . (c6 + 1)) - ((Partial_Sums c3) . (c6 + 1)) by NORMSP_1:def 6
.= (((Partial_Sums c2) . c6) + (c2 . (c6 + 1))) - ((Partial_Sums c3) . (c6 + 1)) by E1
.= (((Partial_Sums c2) . c6) + (c2 . (c6 + 1))) - ((c3 . (c6 + 1)) + ((Partial_Sums c3) . c6)) by E1
.= ((((Partial_Sums c2) . c6) + (c2 . (c6 + 1))) - (c3 . (c6 + 1))) - ((Partial_Sums c3) . c6) by RLVECT_1:41
.= (((Partial_Sums c2) . c6) + ((c2 . (c6 + 1)) - (c3 . (c6 + 1)))) - ((Partial_Sums c3) . c6) by RLVECT_1:def 6
.= ((Partial_Sums c2) . c6) + (((c2 . (c6 + 1)) - (c3 . (c6 + 1))) - ((Partial_Sums c3) . c6)) by RLVECT_1:def 6
.= ((Partial_Sums c2) . c6) + ((- ((Partial_Sums c3) . c6)) + ((c2 . (c6 + 1)) - (c3 . (c6 + 1))))
.= (((Partial_Sums c2) . c6) + (- ((Partial_Sums c3) . c6))) + ((c2 . (c6 + 1)) - (c3 . (c6 + 1))) by RLVECT_1:def 6
.= (((Partial_Sums c2) . c6) - ((Partial_Sums c3) . c6)) + ((c2 . (c6 + 1)) - (c3 . (c6 + 1)))
.= (((Partial_Sums c2) - (Partial_Sums c3)) . c6) + ((c2 . (c6 + 1)) - (c3 . (c6 + 1))) by NORMSP_1:def 6
.= (((Partial_Sums c2) - (Partial_Sums c3)) . c6) + ((c2 - c3) . (c6 + 1)) by NORMSP_1:def 6 ;
end;
hence (Partial_Sums c2) - (Partial_Sums c3) = Partial_Sums (c2 - c3) by E4, E1;
end;

theorem E4: :: BHSP_4:3
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1 holds Partial_Sums (b2 * b3) = b2 * (Partial_Sums b3)
proof
let c1 be RealUnitarySpace;
let c2 be Real;
let c3 be sequence of c1;
set c4 = Partial_Sums c3;
E5: (c2 * (Partial_Sums c3)) . 0 = c2 * ((Partial_Sums c3) . 0) by NORMSP_1:def 8
.= c2 * (c3 . 0) by E1
.= (c2 * c3) . 0 by NORMSP_1:def 8 ;
now
let c5 be Nat;
thus (c2 * (Partial_Sums c3)) . (c5 + 1) = c2 * ((Partial_Sums c3) . (c5 + 1)) by NORMSP_1:def 8
.= c2 * (((Partial_Sums c3) . c5) + (c3 . (c5 + 1))) by E1
.= (c2 * ((Partial_Sums c3) . c5)) + (c2 * (c3 . (c5 + 1))) by RLVECT_1:def 9
.= ((c2 * (Partial_Sums c3)) . c5) + (c2 * (c3 . (c5 + 1))) by NORMSP_1:def 8
.= ((c2 * (Partial_Sums c3)) . c5) + ((c2 * c3) . (c5 + 1)) by NORMSP_1:def 8 ;
end;
hence Partial_Sums (c2 * c3) = c2 * (Partial_Sums c3) by E5, E1;
end;

theorem :: BHSP_4:4
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Partial_Sums (- b2) = - (Partial_Sums b2)
proof
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
Partial_Sums ((- 1) * c2) = (- 1) * (Partial_Sums c2) by E4;
then Partial_Sums (- c2) = (- 1) * (Partial_Sums c2) by BHSP_1:77;
hence Partial_Sums (- c2) = - (Partial_Sums c2) by BHSP_1:77;
end;

theorem :: BHSP_4:5
for b1 being RealUnitarySpace
for b2, b3 being Real
for b4, b5 being sequence of b1 holds (b2 * (Partial_Sums b4)) + (b3 * (Partial_Sums b5)) = Partial_Sums ((b2 * b4) + (b3 * b5))
proof
let c1 be RealUnitarySpace;
let c2, c3 be Real;
let c4, c5 be sequence of c1;
thus (c2 * (Partial_Sums c4)) + (c3 * (Partial_Sums c5)) = (Partial_Sums (c2 * c4)) + (c3 * (Partial_Sums c5)) by E4
.= (Partial_Sums (c2 * c4)) + (Partial_Sums (c3 * c5)) by E4
.= Partial_Sums ((c2 * c4) + (c3 * c5)) by E2 ;
end;

definition
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
attr a2 is summable means :E5: :: BHSP_4:def 2
 Partial_Sums a2 is convergent;
func Sum c2 -> Point of a1 equals :: BHSP_4:def 3
 lim (Partial_Sums a2);
coherence
lim (Partial_Sums c2) is Point of c1 ;
end;

:: deftheorem E5 defines summable BHSP_4:def 2 :
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( b2 is summable iff Partial_Sums b2 is convergent );

:: deftheorem defines Sum BHSP_4:def 3 :
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds Sum b2 = lim (Partial_Sums b2);

theorem :: BHSP_4:6
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds
( ( b2 is summable & b3 is summable ) implies ( ( b2 + b3 is summable & Sum (b2 + b3) = (Sum b2) + (Sum b3) ) ) )
proof
let c1 be RealUnitarySpace;
let c2, c3 be sequence of c1;
assume that
E6: c2 is summable and
E7: c3 is summable ;
E8: Partial_Sums c2 is convergent by E6, E5;
E9: Partial_Sums c3 is convergent by E7, E5;
then (Partial_Sums c2) + (Partial_Sums c3) is convergent by E8, BHSP_2:3;
then Partial_Sums (c2 + c3) is convergent by E2;
hence c2 + c3 is summable by E5;
thus Sum (c2 + c3) = lim (Partial_Sums (c2 + c3))
.= lim ((Partial_Sums c2) + (Partial_Sums c3)) by E2
.= (lim (Partial_Sums c2)) + (lim (Partial_Sums c3)) by E8, E9, BHSP_2:13
.= (Sum c2) + (lim (Partial_Sums c3))
.= (Sum c2) + (Sum c3) ;
end;

theorem :: BHSP_4:7
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds
( ( b2 is summable & b3 is summable ) implies ( ( b2 - b3 is summable & Sum (b2 - b3) = (Sum b2) - (Sum b3) ) ) )
proof
let c1 be RealUnitarySpace;
let c2, c3 be sequence of c1;
assume that
E6: c2 is summable and
E7: c3 is summable ;
E8: Partial_Sums c2 is convergent by E6, E5;
E9: Partial_Sums c3 is convergent by E7, E5;
then (Partial_Sums c2) - (Partial_Sums c3) is convergent by E8, BHSP_2:4;
then Partial_Sums (c2 - c3) is convergent by E3;
hence c2 - c3 is summable by E5;
thus Sum (c2 - c3) = lim (Partial_Sums (c2 - c3))
.= lim ((Partial_Sums c2) - (Partial_Sums c3)) by E3
.= (lim (Partial_Sums c2)) - (lim (Partial_Sums c3)) by E8, E9, BHSP_2:14
.= (Sum c2) - (lim (Partial_Sums c3))
.= (Sum c2) - (Sum c3) ;
end;

theorem :: BHSP_4:8
for b1 being RealUnitarySpace
for b2 being Real
for b3 being sequence of b1 holds
( b3 is summable implies ( b2 * b3 is summable & Sum (b2 * b3) = b2 * (Sum b3) ) )
proof
let c1 be RealUnitarySpace;
let c2 be Real;
let c3 be sequence of c1;
assume c3 is summable ;
then E6: Partial_Sums c3 is convergent by E5;
then c2 * (Partial_Sums c3) is convergent by BHSP_2:5;
then Partial_Sums (c2 * c3) is convergent by E4;
hence c2 * c3 is summable by E5;
thus Sum (c2 * c3) = lim (Partial_Sums (c2 * c3))
.= lim (c2 * (Partial_Sums c3)) by E4
.= c2 * (lim (Partial_Sums c3)) by E6, BHSP_2:15
.= c2 * (Sum c3) ;
end;

theorem E6: :: BHSP_4:9
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( b2 is summable implies ( b2 is convergent & lim b2 = 0. b1 ) )
proof
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
set c3 = Partial_Sums c2;
assume c2 is summable ;
then E7: Partial_Sums c2 is convergent by E5;
then E8: ( (Partial_Sums c2) ^\ 1 is convergent & lim ((Partial_Sums c2) ^\ 1) = lim (Partial_Sums c2) ) by BHSP_3:44;
then E9: lim (((Partial_Sums c2) ^\ 1) - (Partial_Sums c2)) = (lim (Partial_Sums c2)) - (lim (Partial_Sums c2)) by E7, BHSP_2:14
.= H1(c1) by RLVECT_1:28 ;
E10: c2 ^\ 1 = ((Partial_Sums c2) ^\ 1) - (Partial_Sums c2)
proof
now
let c4 be Nat;
(Partial_Sums c2) . (c4 + 1) = ((Partial_Sums c2) . c4) + (c2 . (c4 + 1)) by E1
.= ((Partial_Sums c2) . c4) + ((c2 ^\ 1) . c4) by BHSP_3:def 5 ;
hence ((Partial_Sums c2) ^\ 1) . c4 = ((Partial_Sums c2) . c4) + ((c2 ^\ 1) . c4) by BHSP_3:def 5;
end;
then E11: (Partial_Sums c2) ^\ 1 = (Partial_Sums c2) + (c2 ^\ 1) by NORMSP_1:def 5;
(c2 ^\ 1) + ((Partial_Sums c2) - (Partial_Sums c2)) = c2 ^\ 1
proof
now
let c4 be Nat;
thus ((c2 ^\ 1) + ((Partial_Sums c2) - (Partial_Sums c2))) . c4 = ((c2 ^\ 1) . c4) + (((Partial_Sums c2) - (Partial_Sums c2)) . c4) by NORMSP_1:def 5
.= ((c2 ^\ 1) . c4) + (((Partial_Sums c2) . c4) - ((Partial_Sums c2) . c4)) by NORMSP_1:def 6
.= ((c2 ^\ 1) . c4) + H1(c1) by RLVECT_1:28
.= (c2 ^\ 1) . c4 by RLVECT_1:10 ;
end;
hence (c2 ^\ 1) + ((Partial_Sums c2) - (Partial_Sums c2)) = c2 ^\ 1 by FUNCT_2:113;
end;
hence c2 ^\ 1 = ((Partial_Sums c2) ^\ 1) - (Partial_Sums c2) by E11, BHSP_1:83;
end;
then c2 ^\ 1 is convergent by E7, E8, BHSP_2:4;
hence E11: c2 is convergent by BHSP_3:46;
c2 ^\ 1 is subsequence of c2 by BHSP_3:43;
hence lim c2 = 0. c1 by E9, E10, E11, BHSP_3:33;
end;

theorem E7: :: BHSP_4:10
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( b1 is_Hilbert_space implies ( b2 is summable iff for b3 being Real holds
not ( b3 > 0 & ( for b4 being Nat holds
ex b5, b6 being Nat st
( b5 >= b4 & b6 >= b4 & not ||.(((Partial_Sums b2) . b5) - ((Partial_Sums b2) . b6)).|| < b3 ) ) ) ) )
proof
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
assume c1 is_Hilbert_space ;
then E8: ( c1 is RealUnitarySpace & c1 is_complete_space ) by BHSP_3:def 7;
set c3 = Partial_Sums c2;
thus ( c2 is summable implies for b1 being Real holds
not ( b1 > 0 & ( for b2 being Nat holds
ex b3, b4 being Nat st
( b3 >= b2 & b4 >= b2 & not ||.(((Partial_Sums c2) . b3) - ((Partial_Sums c2) . b4)).|| < b1 ) ) ) )
proof
assume c2 is summable ;
then Partial_Sums c2 is convergent by E5;
then Partial_Sums c2 is_Cauchy_sequence by BHSP_3:9;
hence for b1 being Real holds
not ( b1 > 0 & ( for b2 being Nat holds
ex b3, b4 being Nat st
( b3 >= b2 & b4 >= b2 & not ||.(((Partial_Sums c2) . b3) - ((Partial_Sums c2) . b4)).|| < b1 ) ) ) by BHSP_3:2;
end;
thus ( ( for b1 being Real holds
not ( b1 > 0 & ( for b2 being Nat holds
ex b3, b4 being Nat st
( b3 >= b2 & b4 >= b2 & not ||.(((Partial_Sums c2) . b3) - ((Partial_Sums c2) . b4)).|| < b1 ) ) ) ) implies c2 is summable )
proof
assume for b1 being Real holds
not ( b1 > 0 & ( for b2 being Nat holds
ex b3, b4 being Nat st
( b3 >= b2 & b4 >= b2 & not ||.(((Partial_Sums c2) . b3) - ((Partial_Sums c2) . b4)).|| < b1 ) ) ) ;
then Partial_Sums c2 is_Cauchy_sequence by BHSP_3:2;
then Partial_Sums c2 is convergent by E8, BHSP_3:def 6;
hence c2 is summable by E5;
end;
end;

theorem :: BHSP_4:11
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( b2 is summable implies Partial_Sums b2 is bounded )
proof
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
assume c2 is summable ;
then Partial_Sums c2 is convergent by E5;
hence Partial_Sums c2 is bounded by BHSP_3:24;
end;

theorem E8: :: BHSP_4:12
for b1 being RealUnitarySpace
for b2, b3 being sequence of b1 holds
( ( for b4 being Nat holds b3 . b4 = b2 . 0 ) implies Partial_Sums (b2 ^\ 1) = ((Partial_Sums b2) ^\ 1) - b3 )
proof
let c1 be RealUnitarySpace;
let c2, c3 be sequence of c1;
assume E9: for b1 being Nat holds c3 . b1 = c2 . 0 ;
E10: (((Partial_Sums c2) ^\ 1) - c3) . 0 = (((Partial_Sums c2) ^\ 1) . 0) - (c3 . 0) by NORMSP_1:def 6
.= (((Partial_Sums c2) ^\ 1) . 0) - (c2 . 0) by E9
.= ((Partial_Sums c2) . (0 + 1)) - (c2 . 0) by BHSP_3:def 5
.= (((Partial_Sums c2) . 0) + (c2 . (0 + 1))) - (c2 . 0) by E1
.= ((c2 . (0 + 1)) + (c2 . 0)) - (c2 . 0) by E1
.= (c2 . (0 + 1)) + ((c2 . 0) - (c2 . 0)) by RLVECT_1:def 6
.= (c2 . (0 + 1)) + H1(c1) by RLVECT_1:28
.= c2 . (0 + 1) by RLVECT_1:10
.= (c2 ^\ 1) . 0 by BHSP_3:def 5 ;
now
let c4 be Nat;
thus (((Partial_Sums c2) ^\ 1) - c3) . (c4 + 1) = (((Partial_Sums c2) ^\ 1) . (c4 + 1)) - (c3 . (c4 + 1)) by NORMSP_1:def 6
.= (((Partial_Sums c2) ^\ 1) . (c4 + 1)) - (c2 . 0) by E9
.= ((Partial_Sums c2) . ((c4 + 1) + 1)) - (c2 . 0) by BHSP_3:def 5
.= ((c2 . ((c4 + 1) + 1)) + ((Partial_Sums c2) . (c4 + 1))) - (c2 . 0) by E1
.= ((c2 . ((c4 + 1) + 1)) + ((Partial_Sums c2) . (c4 + 1))) - (c3 . c4) by E9
.= (c2 . ((c4 + 1) + 1)) + (((Partial_Sums c2) . (c4 + 1)) - (c3 . c4)) by RLVECT_1:def 6
.= (c2 . ((c4 + 1) + 1)) + ((((Partial_Sums c2) ^\ 1) . c4) - (c3 . c4)) by BHSP_3:def 5
.= (c2 . ((c4 + 1) + 1)) + ((((Partial_Sums c2) ^\ 1) - c3) . c4) by NORMSP_1:def 6
.= ((((Partial_Sums c2) ^\ 1) - c3) . c4) + ((c2 ^\ 1) . (c4 + 1)) by BHSP_3:def 5 ;
end;
hence Partial_Sums (c2 ^\ 1) = ((Partial_Sums c2) ^\ 1) - c3 by E10, E1;
end;

theorem E9: :: BHSP_4:13
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( b2 is summable implies for b3 being Nat holds b2 ^\ b3 is summable )
proof
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
defpred S1[ Nat] means c2 ^\ a1 is summable;
assume c2 is summable ;
then E10: S1[0] by BHSP_3:35;
E11: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c3 be Nat;
assume c2 ^\ c3 is summable ;
then Partial_Sums (c2 ^\ c3) is convergent by E5;
then E12: (Partial_Sums (c2 ^\ c3)) ^\ 1 is convergent by BHSP_3:44;
E13: c2 ^\ (c3 + 1) = (c2 ^\ c3) ^\ 1 by BHSP_3:37;
reconsider c4 = NAT --> ((c2 ^\ c3) . 0) as sequence of c1 by FUNCOP_1:57;
E14: for b1 being Nat holds c4 . b1 = (c2 ^\ c3) . 0 by FUNCOP_1:13;
E15: c4 is convergent by BHSP_2:1;
Partial_Sums ((c2 ^\ c3) ^\ 1) = ((Partial_Sums (c2 ^\ c3)) ^\ 1) - c4 by E14, E8;
then Partial_Sums ((c2 ^\ c3) ^\ 1) is convergent by E12, E15, BHSP_2:4;
hence S1[c3 + 1] by E13, E5;
end;
thus for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E10, E11);
end;

theorem :: BHSP_4:14
for b1 being RealUnitarySpace
for b2 being sequence of b1 holds
( ex b3 being Nat st b2 ^\ b3 is summable implies b2 is summable )
proof
let c1 be RealUnitarySpace;
let c2 be sequence of c1;
given c3 being Nat such that E10: c2 ^\ c3 is summable ;
(c2 ^\ c3) ^\ 1 is summable by E10, E9;
then E11: Partial_Sums ((c2 ^\ c3) ^\ 1) is convergent by E5;
reconsider c4 = NAT --> ((Partial_Sums c2) . c3) as sequence of c1 by FUNCOP_1:57;
E12: for b1 being Nat holds c4 . b1 = (Partial_Sums c2) . c3 by FUNCOP_1:13;
E13: c4 is convergent by BHSP_2:1;
defpred S1[ Nat] means ((Partial_Sums c2) ^\ (c3 + 1)) . a1 = ((Partial_Sums (c2 ^\ (c3 + 1))) . a1) + (c4 . a1);
for b1 being Nat holds
S1[b1]
proof
E14: (Partial_Sums (c2 ^\ (c3 + 1))) . 0 = (c2 ^\ (c3 + 1)) . 0 by E1
.= c2 . (0 + (c3 + 1)) by BHSP_3:def 5
.= c2 . (c3 + 1) ;
((Partial_Sums c2) ^\ (c3 + 1)) . 0 = (Partial_Sums c2) . (0 + (c3 + 1)) by BHSP_3:def 5
.= ((Partial_Sums c2) . c3) + (c2 . (c3 + 1)) by E1
.= ((Partial_Sums (c2 ^\ (c3 + 1))) . 0) + (c4 . 0) by E12, E14 ;
then E15: S1[0] ;
E16: now
let c5 be Nat;
assume E17: S1[c5] ;
((Partial_Sums (c2 ^\ (c3 + 1))) . (c5 + 1)) + (c4 . (c5 + 1)) = (c4 . (c5 + 1)) + (((Partial_Sums (c2 ^\ (c3 + 1))) . c5) + ((c2 ^\ (c3 + 1)) . (c5 + 1))) by E1
.= ((c4 . (c5 + 1)) + ((Partial_Sums (c2 ^\ (c3 + 1))) . c5)) + ((c2 ^\ (c3 + 1)) . (c5 + 1)) by RLVECT_1:def 6
.= (((Partial_Sums c2) . c3) + ((Partial_Sums (c2 ^\ (c3 + 1))) . c5)) + ((c2 ^\ (c3 + 1)) . (c5 + 1)) by E12
.= (((Partial_Sums c2) ^\ (c3 + 1)) . c5) + ((c2 ^\ (c3 + 1)) . (c5 + 1)) by E12, E17
.= ((Partial_Sums c2) . (c5 + (c3 + 1))) + ((c2 ^\ (c3 + 1)) . (c5 + 1)) by BHSP_3:def 5
.= ((Partial_Sums c2) . (c5 + (c3 + 1))) + (c2 . ((c5 + 1) + (c3 + 1))) by BHSP_3:def 5
.= (Partial_Sums c2) . ((c5 + (c3 + 1)) + 1) by E1
.= (Partial_Sums c2) . ((c5 + 1) + (c3 + 1))
.= ((Partial_Sums c2) ^\ (c3 + 1)) . (c5 + 1) by BHSP_3:def 5 ;
hence S1[c5 + 1] ;
end;
thus for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E15, E16);
end;
then (Partial_Sums c2) ^\