let X be Banach_Algebra; :: thesis: for z, w being Element of X
for p being real number st p > 0 holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
let z, w be Element of X; :: thesis: for p being real number st p > 0 holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
let p be real number ; :: thesis: ( p > 0 implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p )
assume A1: p > 0 ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
reconsider pp = p as Real by XREAL_0:def 1;
set p1 = min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))));
A2: 1 <= Sum (||.z.|| rExpSeq ) by Th29;
then 0 * (Sum (||.z.|| rExpSeq )) < 4 * (Sum (||.z.|| rExpSeq )) by XREAL_1:70;
then A3: 0 / (4 * (Sum (||.z.|| rExpSeq ))) < p / (4 * (Sum (||.z.|| rExpSeq ))) by A1, XREAL_1:76;
A4: 1 <= Sum (||.w.|| rExpSeq ) by Th29;
then 0 * (Sum (||.w.|| rExpSeq )) < 4 * (Sum (||.w.|| rExpSeq )) by XREAL_1:70;
then 0 / (4 * (Sum (||.w.|| rExpSeq ))) < p / (4 * (Sum (||.w.|| rExpSeq ))) by A1, XREAL_1:76;
then A5: min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) > 0 by A3, XXREAL_0:15;
Partial_Sums (w rExpSeq ) is convergent by LOPBAN_3:def 2;
then for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums (w rExpSeq )) . m) - ((Partial_Sums (w rExpSeq )) . n)).|| < s by LOPBAN_3:4;
then Partial_Sums (w rExpSeq ) is CCauchy by LOPBAN_3:5;
then consider n2 being Element of NAT such that
A6: for k, l being Element of NAT st n2 <= k & n2 <= l holds
||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . l)).|| < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A5, RSSPACE3:10;
||.z.|| rExpSeq is summable by SIN_COS:49;
then Partial_Sums (||.z.|| rExpSeq ) is convergent by SERIES_1:def 2;
then consider n1 being Element of NAT such that
A7: for k, l being Element of NAT st n1 <= k & n1 <= l holds
abs (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . l)) < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A5, COMSEQ_3:4;
set n3 = n1 + n2;
take n4 = (n1 + n2) + (n1 + n2); :: thesis: for k being Element of NAT st n4 <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p

A8: now

let n, k be Element of NAT ; :: thesis: for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).||

now

let l be Element of NAT ; :: thesis: ( l <= k implies ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| )
assume A9: l <= k ; :: thesis: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).||
A10: ||.(((z rExpSeq ) . l) * (((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l)))).|| <= ||.((z rExpSeq ) . l).|| * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| by LOPBAN_3:43;
0 <= ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| by NORMSP_1:8;
then A11: ||.((z rExpSeq ) . l).|| * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| by Th14, XREAL_1:66;
||.(Conj k,z,w).|| . l = ||.((Conj k,z,w) . l).|| by NORMSP_0:def 4
.= ||.(((z rExpSeq ) . l) * (((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l)))).|| by A9, Def9 ;
hence ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| by A10, A11, XXREAL_0:2; :: thesis: verum

end;

hence for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| ; :: thesis: verum

end;

A12: now

let k be Element of NAT ; :: thesis: for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq )))

now

let l be Element of NAT ; :: thesis: ( l <= k implies ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) )
A13: ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| <= ||.((Partial_Sums (w rExpSeq )) . k).|| + ||.((Partial_Sums (w rExpSeq )) . (k -' l)).|| by NORMSP_1:7;
||.((Partial_Sums (w rExpSeq )) . (k -' l)).|| <= Sum (||.w.|| rExpSeq ) by Th28;
then A14: (Sum (||.w.|| rExpSeq )) + ||.((Partial_Sums (w rExpSeq )) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq )) + (Sum (||.w.|| rExpSeq )) by XREAL_1:8;
||.((Partial_Sums (w rExpSeq )) . k).|| <= Sum (||.w.|| rExpSeq ) by Th28;
then ||.((Partial_Sums (w rExpSeq )) . k).|| + ||.((Partial_Sums (w rExpSeq )) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq )) + ||.((Partial_Sums (w rExpSeq )) . (k -' l)).|| by XREAL_1:8;
then ||.((Partial_Sums (w rExpSeq )) . k).|| + ||.((Partial_Sums (w rExpSeq )) . (k -' l)).|| <= 2 * (Sum (||.w.|| rExpSeq )) by A14, XXREAL_0:2;
then A15: ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| <= 2 * (Sum (||.w.|| rExpSeq )) by A13, XXREAL_0:2;
assume l <= k ; :: thesis: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq )))
then A16: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| by A8;
0 <= (||.z.|| rExpSeq ) . l by Th27;
then ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) by A15, XREAL_1:66;
hence ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) by A16, XXREAL_0:2; :: thesis: verum

end;

hence for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) ; :: thesis: verum

end;

now

0 < p / 4 by A1, XREAL_1:226;
then A17: 0 + (p / 4) < (p / 4) + (p / 4) by XREAL_1:8;
A18: 0 <> Sum (||.z.|| rExpSeq ) by Th29;
A19: (Sum (||.z.|| rExpSeq )) * (p / (4 * (Sum (||.z.|| rExpSeq )))) = (Sum (||.z.|| rExpSeq )) * (p * ((4 * (Sum (||.z.|| rExpSeq ))) " )) by XCMPLX_0:def 9
.= ((Sum (||.z.|| rExpSeq )) * p) * ((4 * (Sum (||.z.|| rExpSeq ))) " )
.= ((Sum (||.z.|| rExpSeq )) * p) / (4 * (Sum (||.z.|| rExpSeq ))) by XCMPLX_0:def 9
.= p / 4 by A18, XCMPLX_1:92 ;
let k be Element of NAT ; :: thesis: ( n4 <= k implies abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p )
assume A20: n4 <= k ; :: thesis: abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
A21: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then k -' (n1 + n2) = k - (n1 + n2) by A20, XREAL_1:235, XXREAL_0:2;
then A22: k = (k -' (n1 + n2)) + (n1 + n2) ;
A23: n1 + n2 <= k by A20, A21, XXREAL_0:2;

now

let l be Element of NAT ; :: thesis: ( l <= n1 + n2 implies ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l) )
A24: 0 + n2 <= n1 + n2 by XREAL_1:8;
0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then n2 <= n4 by A24, XXREAL_0:2;
then A25: n2 <= k by A20, XXREAL_0:2;
A26: 0 <= (||.z.|| rExpSeq ) . l by Th27;
assume A27: l <= n1 + n2 ; :: thesis: ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l)
then A28: ((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by XREAL_1:12;
l <= k by A23, A27, XXREAL_0:2;
then A29: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| by A8;
n4 - l <= k - l by A20, XREAL_1:11;
then A30: n1 + n2 <= k - l by A28, XXREAL_0:2;
k -' l = k - l by A23, A27, XREAL_1:235, XXREAL_0:2;
then n2 <= k -' l by A24, A30, XXREAL_0:2;
then ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A6, A25;
then ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))).|| <= ((||.z.|| rExpSeq ) . l) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A26, XREAL_1:66;
hence ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l) by A29, XXREAL_0:2; :: thesis: verum

end;

then A31: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by COMSEQ_3:7;
A32: n1 + 0 <= n1 + n2 by XREAL_1:8;
then n1 <= k by A23, XXREAL_0:2;
then abs (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) <= min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A7, A32;
then ((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) <= min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A20, A21, Th30, XXREAL_0:2;
then A33: (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq ))) <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * (2 * (Sum (||.w.|| rExpSeq ))) by A4, XREAL_1:66;
for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= (2 * (Sum (||.w.|| rExpSeq ))) * ((||.z.|| rExpSeq ) . l) by A12;
then ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq ))) by A22, COMSEQ_3:8;
then A34: ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * (2 * (Sum (||.w.|| rExpSeq ))) by A33, XXREAL_0:2;
A35: 0 <> Sum (||.w.|| rExpSeq ) by Th29;
((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A5, Th28, XREAL_1:66;
then A36: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= (Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A31, XXREAL_0:2;
(Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (Sum (||.z.|| rExpSeq )) * (p / (4 * (Sum (||.z.|| rExpSeq )))) by A2, XREAL_1:66, XXREAL_0:17;
then (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= p / 4 by A36, A19, XXREAL_0:2;
then A37: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) < p / 2 by A17, XXREAL_0:2;
0 * (Sum (||.w.|| rExpSeq )) < 2 * (Sum (||.w.|| rExpSeq )) by A4, XREAL_1:70;
then A38: (2 * (Sum (||.w.|| rExpSeq ))) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (2 * (Sum (||.w.|| rExpSeq ))) * (p / (4 * (Sum (||.w.|| rExpSeq )))) by XREAL_1:66, XXREAL_0:17;
(2 * (Sum (||.w.|| rExpSeq ))) * (p / (4 * (Sum (||.w.|| rExpSeq )))) = (2 * (Sum (||.w.|| rExpSeq ))) * (p * ((4 * (Sum (||.w.|| rExpSeq ))) " )) by XCMPLX_0:def 9
.= ((2 * (Sum (||.w.|| rExpSeq ))) * p) * ((4 * (Sum (||.w.|| rExpSeq ))) " )
.= ((2 * p) * (Sum (||.w.|| rExpSeq ))) / (4 * (Sum (||.w.|| rExpSeq ))) by XCMPLX_0:def 9
.= (2 * p) / 4 by A35, XCMPLX_1:92
.= p / 2 ;
then ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= p / 2 by A34, A38, XXREAL_0:2;
then (((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2))) + ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) < (p / 2) + (p / 2) by A37, XREAL_1:10;
hence abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p by Th31; :: thesis: verum

end;

hence for k being Element of NAT st n4 <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p ; :: thesis: verum