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

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