let i be Element of 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)
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
A1: i in dom f and
A2: i + 1 in dom f ; :: thesis: f /. i <> f /. (i + 1)
A3: f is_sequence_on GoB f by GOBOARD5:def 5;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. i = (GoB f) * i1,j1 by A1, GOBOARD1:def 11;
consider i2, j2 being Element of NAT such that
A6: [i2,j2] in Indices (GoB f) and
A7: f /. (i + 1) = (GoB f) * i2,j2 by A2, A3, GOBOARD1:def 11;
assume f /. i = f /. (i + 1) ; :: thesis: contradiction
then ( i1 = i2 & j1 = j2 ) by A4, A5, A6, A7, GOBOARD1:21;
then ( i1 - i2 = 0 & j1 - j2 = 0 ) ;
then A8: (abs 0 ) + (abs 0 ) = 1 by A1, A2, A3, A4, A5, A7, GOBOARD1:def 11;
abs 0 = 0 by ABSVALUE:7;
hence contradiction by A8; :: thesis: verum