given g1, g2 being Real such that A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < p and
A3: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g2).| < p and
A4: g1 <> g2 ; :: thesis: contradiction

A5: now :: thesis: not |.(g1 - g2).| = 0

assume |.(g1 - g2).| = 0 ; :: thesis: contradiction
then 0 + g2 = (g1 - g2) + g2 by ABSVALUE:2;
hence contradiction by A4; :: thesis: verum

end;

A6: 0 <= |.(g1 - g2).| by COMPLEX1:46;
then consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < |.(g1 - g2).| / 4 by A2, A5;
consider n2 being Nat such that
A8: for m being Nat st n2 <= m holds
|.((seq . m) - g2).| < |.(g1 - g2).| / 4 by A3, A5, A6;
A9: |.((seq . (n1 + n2)) - g1).| < |.(g1 - g2).| / 4 by A7, NAT_1:12;
|.((seq . (n1 + n2)) - g2).| < |.(g1 - g2).| / 4 by A8, NAT_1:12;
then A10: |.((seq . (n1 + n2)) - g2).| + |.((seq . (n1 + n2)) - g1).| < (|.(g1 - g2).| / 4) + (|.(g1 - g2).| / 4) by A9, XREAL_1:8;
|.(g1 - g2).| = |.((- ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).| ;
then |.(g1 - g2).| <= |.(- ((seq . (n1 + n2)) - g1)).| + |.((seq . (n1 + n2)) - g2).| by COMPLEX1:56;
then A11: |.(g1 - g2).| <= |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).| by COMPLEX1:52;
|.(g1 - g2).| / 2 < |.(g1 - g2).| by A5, A6, XREAL_1:216;
hence contradiction by A10, A11, XXREAL_0:2; :: thesis: verum