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
; 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; verum