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).| > 0 by A4, COMPLEX1:62;
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((s . m) - g1).| < p by A2;
consider n2 being Nat such that
A7: for m being Nat st n2 <= m holds
|.((s . m) - g2).| < p by A3, A5;
reconsider n = max (n1,n2) as Element of NAT by ORDINAL1:def 12;
for m being Nat st n <= m holds
2 * p < 2 * p

proof

let m be 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:7;
then n2 <= m by XREAL_1:6;
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:57;
then A10: |.(g1 - g2).| <= |.((s . m) - g1).| + |.(g2 - (s . m)).| by COMPLEX1:60;
n1 <= n by XXREAL_0:25;
then n + n1 <= n + m by A8, XREAL_1:7;
then n1 <= m by XREAL_1:6;
then |.((s . m) - g1).| < p by A6;
then |.((s . m) - g1).| + |.((s . m) - g2).| < p + p by A9, XREAL_1:8;
hence 2 * p < 2 * p by A10, COMPLEX1:60; :: thesis: verum

end;

hence contradiction ; :: thesis: verum