let i, j, n be Element of NAT ; :: thesis: for G being Go-board st [i,j] in Indices G & [(i + n),j] in Indices G holds
dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 )
let G be Go-board; :: thesis: ( [i,j] in Indices G & [(i + n),j] in Indices G implies dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 ) )
assume that
A1: [i,j] in Indices G and
A2: [(i + n),j] in Indices G ; :: thesis: dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 )
set x = G * i,j;
set y = G * (i + n),j;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 )

hence dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 ) by TOPREAL6:102; :: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: dist (G * i,j),(G * (i + n),j) = ((G * (i + n),j) `1 ) - ((G * i,j) `1 )

A4: i + n <= len G by A2, MATRIX_1:39;
A5: 1 <= i by A1, MATRIX_1:39;
A6: 1 <= i + n by A2, MATRIX_1:39;
A7: ( 1 <= j & j <= width G ) by A1, MATRIX_1:39;
1 <= n by A3, NAT_1:14;
then i < i + n by NAT_1:19;
then (G * i,j) `1 < (G * (i + n),j) `1 by A4, A7, A5, GOBOARD5:4;
then A8: ((G * i,j) `1 ) - ((G * i,j) `1 ) < ((G * (i + n),j) `1 ) - ((G * i,j) `1 ) by XREAL_1:16;
i <= len G by A1, MATRIX_1:39;
then A9: (G * i,j) `2 = (G * 1,j) `2 by A7, A5, GOBOARD5:2
.= (G * (i + n),j) `2 by A6, A4, A7, GOBOARD5:2 ;
thus dist (G * i,j),(G * (i + n),j) = sqrt (((((G * i,j) `1 ) - ((G * (i + n),j) `1 )) ^2 ) + ((((G * i,j) `2 ) - ((G * (i + n),j) `2 )) ^2 )) by TOPREAL6:101
.= abs (((G * i,j) `1 ) - ((G * (i + n),j) `1 )) by A9, COMPLEX1:158
.= abs (- (((G * i,j) `1 ) - ((G * (i + n),j) `1 ))) by COMPLEX1:138
.= ((G * (i + n),j) `1 ) - ((G * i,j) `1 ) by A8, ABSVALUE:def 1 ; :: thesis: verum

end;

end;