let n be Element of NAT ; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
let k be Element of NAT ; :: thesis:
assume A1: ( 1 <= k & k + 1 <= len f ) ; :: thesis:
assume f is_sequence_on Gauge C,n ; :: thesis:
then consider i1, j1, i2, j2 being Element of NAT such that
A2: [i1,j1] in Indices (Gauge C,n) and
A3: f /. k = (Gauge C,n) * i1,j1 and
A4: [i2,j2] in Indices (Gauge C,n) and
A5: f /. (k + 1) = (Gauge C,n) * i2,j2 and
A6: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, JORDAN8:6;

per cases by A6;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

hence ( dist (f /. k),(f /. (k + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n) or dist (f /. k),(f /. (k + 1)) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A2, A3, A4, A5, GOBRD14:19; :: thesis:

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

hence ( dist (f /. k),(f /. (k + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n) or dist (f /. k),(f /. (k + 1)) = ((E-bound C) - (W-bound C)) / (2 |^ n) ) by A2, A3, A4, A5, GOBRD14:20; :: thesis:

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

end;