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