let C be Simple_closed_curve; :: thesis: for i, j, n being 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 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_0:32;
1 <= j by A1, MATRIX_0:32;
then A4: 1 <= width (Gauge (C,n)) by A3, XXREAL_0:2;
A5: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then 2 <= len (Gauge (C,n)) by XXREAL_0:2;
then A6: [2,1] in Indices (Gauge (C,n)) by A4, MATRIX_0:30;
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:10;
1 <= len (Gauge (C,n)) by A5, XXREAL_0:2;
then [1,1] in Indices (Gauge (C,n)) by A4, MATRIX_0:30;
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:10
.= (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) by A1, A2, GOBRD14:5 ;
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