let i, j, n be 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);

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 )
;

end;

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:93; :: 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_0:32;

A5: 1 <= i by A1, MATRIX_0:32;

A6: 1 <= i + n by A2, MATRIX_0:32;

A7: ( 1 <= j & j <= width G ) by A1, MATRIX_0:32;

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:3;

then A8: ((G * (i,j)) `1) - ((G * (i,j)) `1) < ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by XREAL_1:14;

i <= len G by A1, MATRIX_0:32;

then A9: (G * (i,j)) `2 = (G * (1,j)) `2 by A7, A5, GOBOARD5:1

.= (G * ((i + n),j)) `2 by A6, A4, A7, GOBOARD5:1 ;

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:92

.= |.(((G * (i,j)) `1) - ((G * ((i + n),j)) `1)).| by A9, COMPLEX1:72

.= |.(- (((G * (i,j)) `1) - ((G * ((i + n),j)) `1))).| by COMPLEX1:52

.= ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by A8, ABSVALUE:def 1 ; :: thesis: verum

end;A5: 1 <= i by A1, MATRIX_0:32;

A6: 1 <= i + n by A2, MATRIX_0:32;

A7: ( 1 <= j & j <= width G ) by A1, MATRIX_0:32;

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:3;

then A8: ((G * (i,j)) `1) - ((G * (i,j)) `1) < ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by XREAL_1:14;

i <= len G by A1, MATRIX_0:32;

then A9: (G * (i,j)) `2 = (G * (1,j)) `2 by A7, A5, GOBOARD5:1

.= (G * ((i + n),j)) `2 by A6, A4, A7, GOBOARD5:1 ;

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:92

.= |.(((G * (i,j)) `1) - ((G * ((i + n),j)) `1)).| by A9, COMPLEX1:72

.= |.(- (((G * (i,j)) `1) - ((G * ((i + n),j)) `1))).| by COMPLEX1:52

.= ((G * ((i + n),j)) `1) - ((G * (i,j)) `1) by A8, ABSVALUE:def 1 ; :: thesis: verum