let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n)
let f be FinSequence of (TOP-REAL 2); :: thesis: for k being Nat st 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n)
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on Gauge (C,n) & not dist ((f /. k),(f /. (k + 1))) = ((N-bound C) - (S-bound C)) / (2 |^ n) implies dist ((f /. k),(f /. (k + 1))) = ((E-bound C) - (W-bound C)) / (2 |^ n) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; :: thesis: ( not f is_sequence_on Gauge (C,n) or 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) )
assume f is_sequence_on Gauge (C,n) ; :: thesis: ( 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) )
then consider i1, j1, i2, j2 being Nat such that
A3: [i1,j1] in Indices (Gauge (C,n)) and
A4: f /. k = (Gauge (C,n)) * (i1,j1) and
A5: [i2,j2] in Indices (Gauge (C,n)) and
A6: f /. (k + 1) = (Gauge (C,n)) * (i2,j2) and
A7: ( ( 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, A2, JORDAN8:3;
per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A7;
suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ( 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) )
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 A3, A4, A5, A6, GOBRD14:9; :: thesis: verum
end;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( 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) )
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 A3, A4, A5, A6, GOBRD14:10; :: thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( 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) )
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 A3, A4, A5, A6, GOBRD14:10; :: thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( 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) )
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 A3, A4, A5, A6, GOBRD14:9; :: thesis: verum
end;
end;