let g1, g2 be Element of COMPLEX ; :: thesis: ( ( for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g1).| < p ) & ( for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of NAT st n1 <= m holds
|.((s . m) - g1).| < p and
A3: for p being Real st 0 < p holds
ex n2 being Element of NAT st
for m being Element of 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).| > 0 by A4, COMPLEX1:148;
then consider n1 being Element of NAT such that
A6: for m being Element of NAT st n1 <= m holds
|.((s . m) - g1).| < p by A2, XREAL_1:141;
consider n2 being Element of NAT such that
A7: for m being Element of NAT st n2 <= m holds
|.((s . m) - g2).| < p by A3, A5, XREAL_1:141;
reconsider n = max n1,n2 as Element of NAT by FINSEQ_2:1;
for m being Element of NAT st n <= m holds
2 * p < 2 * p

proof

let m be Element of NAT ; :: thesis: ( n <= m implies 2 * p < 2 * p )
assume A8: n <= m ; :: thesis: 2 * p < 2 * p
n2 <= n by XXREAL_0:25;
then n + n2 <= n + m by A8, XREAL_1:9;
then n2 <= m by XREAL_1:8;
then A9: |.((s . m) - g2).| < p by A7;
|.(g1 - g2).| = |.((g1 - (s . m)) - (g2 - (s . m))).| ;
then |.(g1 - g2).| <= |.(g1 - (s . m)).| + |.(g2 - (s . m)).| by COMPLEX1:143;
then A10: |.(g1 - g2).| <= |.((s . m) - g1).| + |.(g2 - (s . m)).| by COMPLEX1:146;
n1 <= n by XXREAL_0:25;
then n + n1 <= n + m by A8, XREAL_1:9;
then n1 <= m by XREAL_1:8;
then |.((s . m) - g1).| < p by A6;
then |.((s . m) - g1).| + |.((s . m) - g2).| < p + p by A9, XREAL_1:10;
hence 2 * p < 2 * p by A10, COMPLEX1:146; :: thesis: verum

end;

hence contradiction ; :: thesis: verum