given g1, g2 being Element of M such that A2:
for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S1 . m),g1) < r and

A3: for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S1 . m),g2) < r and

A4: g1 <> g2 ; :: thesis: contradiction

set a = (dist (g1,g2)) / 4;

A5: dist (g1,g2) >= 0 by METRIC_1:5;

A6: dist (g1,g2) <> 0 by A4, METRIC_1:2;

then consider n1 being Nat such that

A7: for m being Nat st n1 <= m holds

dist ((S1 . m),g1) < (dist (g1,g2)) / 4 by A2, A5, XREAL_1:224;

consider n2 being Nat such that

A8: for m being Nat st n2 <= m holds

dist ((S1 . m),g2) < (dist (g1,g2)) / 4 by A3, A6, A5, XREAL_1:224;

set k = n1 + n2;

A9: dist ((S1 . (n1 + n2)),g2) < (dist (g1,g2)) / 4 by A8, NAT_1:12;

A10: dist (g1,g2) <= (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) by METRIC_1:4;

dist ((S1 . (n1 + n2)),g1) < (dist (g1,g2)) / 4 by A7, NAT_1:12;

then (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) < ((dist (g1,g2)) / 4) + ((dist (g1,g2)) / 4) by A9, XREAL_1:8;

then dist (g1,g2) < (dist (g1,g2)) / 2 by A10, XXREAL_0:2;

hence contradiction by A6, A5, XREAL_1:216; :: thesis: verum

ex n being Nat st

for m being Nat st n <= m holds

dist ((S1 . m),g1) < r and

A3: for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S1 . m),g2) < r and

A4: g1 <> g2 ; :: thesis: contradiction

set a = (dist (g1,g2)) / 4;

A5: dist (g1,g2) >= 0 by METRIC_1:5;

A6: dist (g1,g2) <> 0 by A4, METRIC_1:2;

then consider n1 being Nat such that

A7: for m being Nat st n1 <= m holds

dist ((S1 . m),g1) < (dist (g1,g2)) / 4 by A2, A5, XREAL_1:224;

consider n2 being Nat such that

A8: for m being Nat st n2 <= m holds

dist ((S1 . m),g2) < (dist (g1,g2)) / 4 by A3, A6, A5, XREAL_1:224;

set k = n1 + n2;

A9: dist ((S1 . (n1 + n2)),g2) < (dist (g1,g2)) / 4 by A8, NAT_1:12;

A10: dist (g1,g2) <= (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) by METRIC_1:4;

dist ((S1 . (n1 + n2)),g1) < (dist (g1,g2)) / 4 by A7, NAT_1:12;

then (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) < ((dist (g1,g2)) / 4) + ((dist (g1,g2)) / 4) by A9, XREAL_1:8;

then dist (g1,g2) < (dist (g1,g2)) / 2 by A10, XXREAL_0:2;

hence contradiction by A6, A5, XREAL_1:216; :: thesis: verum