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 that
A1: [i,j] in Indices (Gauge C,n) and
A2: [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 )
A3: 1 <= j + 1 by A2, MATRIX_1:39;
len (Gauge C,n) >= 4 by JORDAN8:13;
then A4: 1 <= len (Gauge C,n) by XXREAL_0:2;
(2 |^ n) + 3 >= 3 by NAT_1:11;
then width (Gauge C,n) >= 3 by JORDAN1A:49;
then 2 <= width (Gauge C,n) by XXREAL_0:2;
then A5: [1,2] in Indices (Gauge C,n) by A4, MATRIX_1:37;
j + 1 <= width (Gauge C,n) by A2, MATRIX_1:39;
then 1 <= width (Gauge C,n) by A3, XXREAL_0:2;
then A6: [1,1] in Indices (Gauge C,n) by A4, 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, A2, 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 A6, A5, GOBRD14:19
.= (((Gauge C,n) * i,(j + 1)) `2 ) - (((Gauge C,n) * i,j) `2 ) by A1, A2, 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