let g1, g2 be Complex; :: thesis: ( ( for p being Real st 0< p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m)- g1).|< p ) & ( for p being Real st 0< p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m)- g2).|< p ) implies g1 = g2 ) assume that A2:
for p being Real st 0< p holds ex n1 being Nat st for m being Nat st n1 <= m holds |.((s . m)- g1).|< p
and A3:
for p being Real st 0< p holds ex n2 being Nat st for m being Nat st n2 <= m holds |.((s . m)- g2).|< p
and A4:
g1 <> g2
; :: thesis: contradiction reconsider p = |.(g1 - g2).|/ 2 as Real ; A5:
|.(g1 - g2).|>0byA4, COMPLEX1:62; then consider n1 being Nat such that A6:
for m being Nat st n1 <= m holds |.((s . m)- g1).|< p
byA2; consider n2 being Nat such that A7:
for m being Nat st n2 <= m holds |.((s . m)- g2).|< p
byA3, A5; reconsider n = max (n1,n2) as Element of NATbyORDINAL1:def 12;
for m being Nat st n <= m holds 2 * p < 2 * p