let C be Simple_closed_curve; :: thesis: for i, j, n being Element of NAT st [i,j] in Indices (Gauge C,n) & [i,(j + 1)] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) = (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 )
let i, j, n be Element of NAT ; :: thesis: ( [i,j] in Indices (Gauge C,n) & [i,(j + 1)] in Indices (Gauge C,n) implies dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) = (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) )
set G = Gauge C,n;
assume A1: ( [i,j] in Indices (Gauge C,n) & [i,(j + 1)] in Indices (Gauge C,n) ) ; :: thesis: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) = (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 )
then A2: ( 1 <= j & j < j + 1 & j + 1 <= width (Gauge C,n) & 1 <= i & i <= len (Gauge C,n) ) by MATRIX_1:39, XREAL_1:31;
1 <= j + 1 by A1, MATRIX_1:39;
then A3: ( 1 <= width (Gauge C,n) & 1 <= i + 1 ) by A2, NAT_1:11, XXREAL_0:2;
A4: len (Gauge C,n) >= 4 by JORDAN8:13;
(2 |^ n) + 3 >= 3 by NAT_1:11;
then width (Gauge C,n) >= 3 by JORDAN1A:49;
then ( 2 <= width (Gauge C,n) & 1 <= len (Gauge C,n) ) by A4, XXREAL_0:2;
then A5: ( [1,1] in Indices (Gauge C,n) & [1,2] in Indices (Gauge C,n) ) by A3, MATRIX_1:37;
dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A1, GOBRD14:19;
then dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,(1 + 1)) = dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) by A5, GOBRD14:19
.= (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) by A1, GOBRD14:16 ;
hence dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) = (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) ; :: thesis: verum