given g1, g2 being Real such that A2: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - g1).| < e and
A3: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - g2).| < e and
A4: g1 <> g2 ; :: thesis: contradiction
A5: now :: thesis: not |.(g1 - g2).| = 0
assume |.(g1 - g2).| = 0 ; :: thesis: contradiction
then g1 - g2 = 0 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 n, m being Nat st N1 <= n & N1 <= m holds
|.((Rseq . (n,m)) - g1).| < |.(g1 - g2).| / 4 by A2, A5;
consider N2 being Nat such that
A8: for n, m being Nat st N2 <= n & N2 <= m holds
|.((Rseq . (n,m)) - g2).| < |.(g1 - g2).| / 4 by A3, A5, A6;
( N1 + N2 >= N1 & N1 + N2 >= N2 ) by NAT_1:11;
then ( |.((Rseq . ((N1 + N2),(N1 + N2))) - g1).| < |.(g1 - g2).| / 4 & |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).| < |.(g1 - g2).| / 4 ) by A7, A8;
then A10: |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).| + |.((Rseq . ((N1 + N2),(N1 + N2))) - g1).| < (|.(g1 - g2).| / 4) + (|.(g1 - g2).| / 4) by XREAL_1:8;
|.(g1 - g2).| = |.((- ((Rseq . ((N1 + N2),(N1 + N2))) - g1)) + ((Rseq . ((N1 + N2),(N1 + N2))) - g2)).| ;
then |.(g1 - g2).| <= |.(- ((Rseq . ((N1 + N2),(N1 + N2))) - g1)).| + |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).| by COMPLEX1:56;
then A11: |.(g1 - g2).| <= |.((Rseq . ((N1 + N2),(N1 + N2))) - g1).| + |.((Rseq . ((N1 + N2),(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