let i be Nat; for f being non empty standard FinSequence of (TOP-REAL 2) st i in dom f & i + 1 in dom f holds
f /. i <> f /. (i + 1)
A1:
|.0.| = 0
by ABSVALUE:2;
let f be non empty standard FinSequence of (TOP-REAL 2); ( i in dom f & i + 1 in dom f implies f /. i <> f /. (i + 1) )
assume that
A2:
i in dom f
and
A3:
i + 1 in dom f
; f /. i <> f /. (i + 1)
A4:
f is_sequence_on GoB f
by GOBOARD5:def 5;
then consider i1, j1 being Nat such that
A5:
( [i1,j1] in Indices (GoB f) & f /. i = (GoB f) * (i1,j1) )
by A2, GOBOARD1:def 9;
consider i2, j2 being Nat such that
A6:
[i2,j2] in Indices (GoB f)
and
A7:
f /. (i + 1) = (GoB f) * (i2,j2)
by A3, A4, GOBOARD1:def 9;
assume A8:
f /. i = f /. (i + 1)
; contradiction
then
j1 = j2
by A5, A6, A7, GOBOARD1:5;
then A9:
j1 - j2 = 0
;
i1 = i2
by A5, A6, A7, A8, GOBOARD1:5;
then
i1 - i2 = 0
;
then
|.0.| + |.0.| = 1
by A2, A3, A4, A5, A7, A9, GOBOARD1:def 9;
hence
contradiction
by A1; verum