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