let i, j, n be Element of NAT ; for G being Go-board st [i,j] in Indices G & [i,(j + n)] in Indices G holds
dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
let G be Go-board; ( [i,j] in Indices G & [i,(j + n)] in Indices G implies dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 ) )
assume that
A1:
[i,j] in Indices G
and
A2:
[i,(j + n)] in Indices G
; dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
set x = G * i,j;
set y = G * i,(j + n);
per cases
( n = 0 or n <> 0 )
;
suppose A3:
n <> 0
;
dist (G * i,j),(G * i,(j + n)) = ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )A4:
j + n <= width G
by A2, MATRIX_1:39;
A5:
( 1
<= i &
i <= len G )
by A1, MATRIX_1:39;
A6:
1
<= j + n
by A2, MATRIX_1:39;
A7:
1
<= j
by A1, MATRIX_1:39;
1
<= n
by A3, NAT_1:14;
then
j < j + n
by NAT_1:19;
then
(G * i,j) `2 < (G * i,(j + n)) `2
by A4, A7, A5, GOBOARD5:5;
then A8:
((G * i,j) `2 ) - ((G * i,j) `2 ) < ((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
by XREAL_1:16;
j <= width G
by A1, MATRIX_1:39;
then A9:
(G * i,j) `1 =
(G * i,1) `1
by A7, A5, GOBOARD5:3
.=
(G * i,(j + n)) `1
by A6, A4, A5, GOBOARD5:3
;
thus dist (G * i,j),
(G * i,(j + n)) =
sqrt (((((G * i,j) `1 ) - ((G * i,(j + n)) `1 )) ^2 ) + ((((G * i,j) `2 ) - ((G * i,(j + n)) `2 )) ^2 ))
by TOPREAL6:101
.=
abs (((G * i,j) `2 ) - ((G * i,(j + n)) `2 ))
by A9, COMPLEX1:158
.=
abs (- (((G * i,j) `2 ) - ((G * i,(j + n)) `2 )))
by COMPLEX1:138
.=
((G * i,(j + n)) `2 ) - ((G * i,j) `2 )
by A8, ABSVALUE:def 1
;
verum end;