given g1, g2 being real number such that A2: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p and
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g2) < p and
A4: g1 <> g2 ; :: thesis: contradiction

A5: now

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

end;

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