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