let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of ()
for f being FinSequence of ()
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))) = (() - ()) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n)

let C be connected compact non horizontal non vertical Subset of (); :: thesis: for f being FinSequence of ()
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))) = (() - ()) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n)

let f be FinSequence of (); :: 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))) = (() - ()) / (2 |^ n) holds
dist ((f /. k),(f /. (k + 1))) = (() - ()) / (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))) = (() - ()) / (2 |^ n) implies dist ((f /. k),(f /. (k + 1))) = (() - ()) / (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))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) )
assume f is_sequence_on Gauge (C,n) ; :: thesis: ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (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 ;
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))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) )
hence ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) ) by ; :: thesis: verum
end;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) )
hence ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) ) by ; :: thesis: verum
end;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) )
hence ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) ) by ; :: thesis: verum
end;
suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) )
hence ( dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) or dist ((f /. k),(f /. (k + 1))) = (() - ()) / (2 |^ n) ) by ; :: thesis: verum
end;
end;