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 ;
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 ;
consider n2 being Nat such that
A8: for m being Nat st n2 <= m holds
dist ((S1 . m),g2) < (dist (g1,g2)) / 4 by ;
set k = n1 + n2;
A9: dist ((S1 . (n1 + n2)),g2) < (dist (g1,g2)) / 4 by ;
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 ;
then (dist (g1,(S1 . (n1 + n2)))) + (dist ((S1 . (n1 + n2)),g2)) < ((dist (g1,g2)) / 4) + ((dist (g1,g2)) / 4) by ;
then dist (g1,g2) < (dist (g1,g2)) / 2 by ;
hence contradiction by A6, A5, XREAL_1:216; :: thesis: verum