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 that
A1: [i,j] in Indices (Gauge C,n) and
A2: [(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 )
A3: j <= width (Gauge C,n) by A1, MATRIX_1:39;
1 <= j by A1, MATRIX_1:39;
then A4: 1 <= width (Gauge C,n) by A3, XXREAL_0:2;
A5: len (Gauge C,n) >= 4 by JORDAN8:13;
then 2 <= len (Gauge C,n) by XXREAL_0:2;
then A6: [2,1] in Indices (Gauge C,n) by A4, MATRIX_1:37;
A7: dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A1, A2, GOBRD14:20;
1 <= len (Gauge C,n) by A5, XXREAL_0:2;
then [1,1] in Indices (Gauge C,n) by A4, MATRIX_1:37;
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 A6, A7, GOBRD14:20
.= (((Gauge C,n) * (i + 1),j) `1 ) - (((Gauge C,n) * i,j) `1 ) by A1, A2, 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