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