let i be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: 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; :: thesis: verum