given g1, g2 being Element of M such that A2: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S1 . m),g1 < r and
A3: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of 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 Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
dist (S1 . m),g1 < (dist g1,g2) / 4 by A2, A5, XREAL_1:226;
consider n2 being Element of NAT such that
A8: for m being Element of NAT st n2 <= m holds
dist (S1 . m),g2 < (dist g1,g2) / 4 by A3, A6, A5, XREAL_1:226;
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:10;
then dist g1,g2 < (dist g1,g2) / 2 by A10, XXREAL_0:2;
hence contradiction by A6, A5, XREAL_1:218; :: thesis: verum