let z, w be Element of COMPLEX ; :: 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;
A2: 1 <= Sum (|.z.| rExpSeq) by Th18;
A3: 0 < Sum (|.w.| rExpSeq) by Th18;
set p1 = min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))));
A4: min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) > 0 by A1, A2, A3, XXREAL_0:15;

now

let k be set ; :: thesis: ( k in NAT implies |.(z ExpSeq).| . k = (|.z.| rExpSeq) . k )
assume A6: k in NAT ; :: thesis: |.(z ExpSeq).| . k = (|.z.| rExpSeq) . k
thus |.(z ExpSeq).| . k = |.((z ExpSeq) . k).| by VALUED_1:18
.= (|.z.| rExpSeq) . k by A6, Th4 ; :: thesis: verum

end;

then |.(z ExpSeq).| = |.z.| rExpSeq by FUNCT_2:18;
then consider n1 being Element of NAT such that
A8: 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 A4, COMSEQ_3:4;
consider n2 being Element of NAT such that
A9: for k, l being Element of NAT st n2 <= k & n2 <= l holds
|.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . l)).| < min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A4, COMSEQ_3:47;
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

A10: 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 ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|

now

let l be Element of NAT ; :: thesis: ( l <= k implies |.(Conj (k,z,w)).| . l = ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| )
assume A12: l <= k ; :: thesis: |.(Conj (k,z,w)).| . l = ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|
thus |.(Conj (k,z,w)).| . l = |.((Conj (k,z,w)) . l).| by VALUED_1:18
.= |.(((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l)))).| by A12, Def17
.= |.((z ExpSeq) . l).| * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| by COMPLEX1:151
.= ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| by Th4 ; :: 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 ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| ; :: thesis: verum

end;

A13: 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))) )
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 ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| by A10;
|.((Partial_Sums (w ExpSeq)) . k).| <= Sum (|.w.| rExpSeq) by Th17;
then A18: |.((Partial_Sums (w ExpSeq)) . k).| + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= (Sum (|.w.| rExpSeq)) + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| by XREAL_1:8;
|.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= Sum (|.w.| rExpSeq) by Th17;
then (Sum (|.w.| rExpSeq)) + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= (Sum (|.w.| rExpSeq)) + (Sum (|.w.| rExpSeq)) by XREAL_1:8;
then ( |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| <= |.((Partial_Sums (w ExpSeq)) . k).| + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| & |.((Partial_Sums (w ExpSeq)) . k).| + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= 2 * (Sum (|.w.| rExpSeq)) ) by A18, COMPLEX1:143, XXREAL_0:2;
then A22: |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| <= 2 * (Sum (|.w.| rExpSeq)) by XXREAL_0:2;
0 <= (|.z.| rExpSeq) . l by Th19;
hence |.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq))) by A16, A22, XREAL_1:66; :: 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

let k be Element of NAT ; :: thesis: ( n4 <= k implies abs ((Partial_Sums |.(Conj (k,z,w)).|) . k) < p )
assume A25: n4 <= k ; :: thesis: abs ((Partial_Sums |.(Conj (k,z,w)).|) . k) < p
A26: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then A27: n1 + n2 <= k by A25, XXREAL_0:2;
A28: n1 + 0 <= n1 + n2 by XREAL_1:8;
then A29: n1 <= k by A27, 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) )
assume A31: l <= n1 + n2 ; :: thesis: |.(Conj (k,z,w)).| . l <= (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) * ((|.z.| rExpSeq) . l)
then A32: k -' l = k - l by A27, XREAL_1:235, XXREAL_0:2;
A33: 0 + n2 <= n1 + n2 by XREAL_1:8;
A34: n4 - l <= k - l by A25, XREAL_1:11;
((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by A31, XREAL_1:12;
then n1 + n2 <= k - l by A34, XXREAL_0:2;
then A37: n2 <= k -' l by A32, A33, XXREAL_0:2;
0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then n2 <= n4 by A33, XXREAL_0:2;
then n2 <= k by A25, XXREAL_0:2;
then A41: |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| < min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A9, A37;
0 <= (|.z.| rExpSeq) . l by Th19;
then ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| <= ((|.z.| rExpSeq) . l) * (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) by A41, XREAL_1:66;
hence |.(Conj (k,z,w)).| . l <= (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) * ((|.z.| rExpSeq) . l) by A10, A27, A31, XXREAL_0:2; :: thesis: verum

end;

then A44: (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;
((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 A4, Th17, XREAL_1:66;
then A46: (Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2) <= (Sum (|.z.| rExpSeq)) * (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) by A44, XXREAL_0:2;
A47: (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;
A48: 0 <> Sum (|.z.| rExpSeq) by Th18;
(Sum (|.z.| rExpSeq)) * (p / (4 * (Sum (|.z.| rExpSeq)))) = ((Sum (|.z.| rExpSeq)) * p) / (4 * (Sum (|.z.| rExpSeq)))
.= p / 4 by A48, XCMPLX_1:92 ;
then A50: (Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2) <= p / 4 by A46, A47, XXREAL_0:2;
0 + (p / 4) < (p / 4) + (p / 4) by A1, XREAL_1:8;
then A52: (Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2) < p / 2 by A50, XXREAL_0:2;
k -' (n1 + n2) = k - (n1 + n2) by A25, A26, XREAL_1:235, XXREAL_0:2;
then A54: k = (k -' (n1 + n2)) + (n1 + n2) ;
for l being Element of NAT st l <= k holds
|.(Conj (k,z,w)).| . l <= (2 * (Sum (|.w.| rExpSeq))) * ((|.z.| rExpSeq) . l) by A13;
then A56: ((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 A54, COMSEQ_3:8;
abs (((Partial_Sums (|.z.| rExpSeq)) . k) - ((Partial_Sums (|.z.| rExpSeq)) . (n1 + n2))) <= min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A8, A28, A29;
then ((Partial_Sums (|.z.| rExpSeq)) . k) - ((Partial_Sums (|.z.| rExpSeq)) . (n1 + n2)) <= min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A25, A26, Th20, XXREAL_0:2;
then (((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 A3, XREAL_1:66;
then A60: ((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 A56, XXREAL_0:2;
A61: (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 A3, XREAL_1:66, XXREAL_0:17;
A62: 0 <> Sum (|.w.| rExpSeq) by Th18;
(2 * (Sum (|.w.| rExpSeq))) * (p / (4 * (Sum (|.w.| rExpSeq)))) = ((2 * p) * (Sum (|.w.| rExpSeq))) / (4 * (Sum (|.w.| rExpSeq)))
.= (p + p) / 4 by A62, XCMPLX_1:92
.= p / 2 ;
then ((Partial_Sums |.(Conj (k,z,w)).|) . k) - ((Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2)) <= p / 2 by A60, A61, 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 A52, XREAL_1:10;
hence abs ((Partial_Sums |.(Conj (k,z,w)).|) . k) < p by Th21; :: 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