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;

A5: 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;

A7: |.(z ExpSeq ).| = |.z.| rExpSeq by A5, FUNCT_2:18;
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, A7, 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))).|

A11: 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;

thus 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))).| by A11; :: 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 )))

A14: now

let l be Element of NAT ; :: thesis: ( l <= k implies |.(Conj k,z,w).| . l <= ((|.z.| rExpSeq ) . l) * (2 * (Sum (|.w.| rExpSeq ))) )
assume A15: l <= k ; :: thesis: |.(Conj k,z,w).| . l <= ((|.z.| rExpSeq ) . l) * (2 * (Sum (|.w.| rExpSeq )))
A16: |.(Conj k,z,w).| . l = ((|.z.| rExpSeq ) . l) * |.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).| by A10, A15;
A17: |.((Partial_Sums (w ExpSeq )) . k).| <= Sum (|.w.| rExpSeq ) by Th17;
A18: |.((Partial_Sums (w ExpSeq )) . k).| + |.((Partial_Sums (w ExpSeq )) . (k -' l)).| <= (Sum (|.w.| rExpSeq )) + |.((Partial_Sums (w ExpSeq )) . (k -' l)).| by A17, XREAL_1:8;
A19: |.((Partial_Sums (w ExpSeq )) . (k -' l)).| <= Sum (|.w.| rExpSeq ) by Th17;
A20: (Sum (|.w.| rExpSeq )) + |.((Partial_Sums (w ExpSeq )) . (k -' l)).| <= (Sum (|.w.| rExpSeq )) + (Sum (|.w.| rExpSeq )) by A19, XREAL_1:8;
A21: ( |.(((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, A20, COMPLEX1:143, XXREAL_0:2;
A22: |.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).| <= 2 * (Sum (|.w.| rExpSeq )) by A21, XXREAL_0:2;
A23: 0 <= (|.z.| rExpSeq ) . l by Th19;
thus |.(Conj k,z,w).| . l <= ((|.z.| rExpSeq ) . l) * (2 * (Sum (|.w.| rExpSeq ))) by A16, A22, A23, XREAL_1:66; :: thesis: verum

end;

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

end;

A24: 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;
A27: n1 + n2 <= k by A25, A26, XXREAL_0:2;
A28: n1 + 0 <= n1 + n2 by XREAL_1:8;
A29: n1 <= k by A27, A28, XXREAL_0:2;

A30: 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)
A32: k -' l = k - l by A27, A31, 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;
A35: ((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by A31, XREAL_1:12;
A36: n1 + n2 <= k - l by A34, A35, XXREAL_0:2;
A37: n2 <= k -' l by A32, A33, A36, XXREAL_0:2;
A38: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
A39: n2 <= n4 by A33, A38, XXREAL_0:2;
A40: n2 <= k by A25, A39, XXREAL_0:2;
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, A40;
A42: 0 <= (|.z.| rExpSeq ) . l by Th19;
A43: ((|.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, A42, XREAL_1:66;
thus |.(Conj k,z,w).| . l <= (min (pp / (4 * (Sum (|.z.| rExpSeq )))),(pp / (4 * (Sum (|.w.| rExpSeq ))))) * ((|.z.| rExpSeq ) . l) by A10, A27, A31, A43, XXREAL_0:2; :: thesis: verum

end;

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 A30, COMSEQ_3:7;
A45: ((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;
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, A45, 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;
A49: (Sum (|.z.| rExpSeq )) * (p / (4 * (Sum (|.z.| rExpSeq )))) = ((Sum (|.z.| rExpSeq )) * p) / (4 * (Sum (|.z.| rExpSeq )))
.= p / 4 by A48, XCMPLX_1:92 ;
A50: (Partial_Sums |.(Conj k,z,w).|) . (n1 + n2) <= p / 4 by A46, A47, A49, XXREAL_0:2;
A51: 0 + (p / 4) < (p / 4) + (p / 4) by A1, XREAL_1:8;
A52: (Partial_Sums |.(Conj k,z,w).|) . (n1 + n2) < p / 2 by A50, A51, XXREAL_0:2;
A53: k -' (n1 + n2) = k - (n1 + n2) by A25, A26, XREAL_1:235, XXREAL_0:2;
A54: k = (k -' (n1 + n2)) + (n1 + n2) by A53;
A55: for l being Element of NAT st l <= k holds
|.(Conj k,z,w).| . l <= (2 * (Sum (|.w.| rExpSeq ))) * ((|.z.| rExpSeq ) . l) by A13;
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, A55, COMSEQ_3:8;
A57: 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;
A58: ((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, A57, Th20, XXREAL_0:2;
A59: (((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, A58, XREAL_1:66;
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, A59, 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;
A63: (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 ;
A64: ((Partial_Sums |.(Conj k,z,w).|) . k) - ((Partial_Sums |.(Conj k,z,w).|) . (n1 + n2)) <= p / 2 by A60, A61, A63, XXREAL_0:2;
A65: (((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, A64, XREAL_1:10;
thus abs ((Partial_Sums |.(Conj k,z,w).|) . k) < p by A65, Th21; :: thesis: verum

end;

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