let i, j, n be Nat; :: thesis: 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; :: thesis: ( [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 ; :: thesis: 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));

dist ((G * (i,j)),(G * (i,(j + n)))) = ((G * (i,(j + n))) `2) - ((G * (i,j)) `2)

let G be Go-board; :: thesis: ( [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 ; :: thesis: 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 )
;

end;

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

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

end;suppose A3:
n <> 0
; :: thesis: 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_0:32;

A5: ( 1 <= i & i <= len G ) by A1, MATRIX_0:32;

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

A7: 1 <= j by A1, MATRIX_0:32;

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

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

j <= width G by A1, MATRIX_0:32;

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

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

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

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

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

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

end;A5: ( 1 <= i & i <= len G ) by A1, MATRIX_0:32;

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

A7: 1 <= j by A1, MATRIX_0:32;

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

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

j <= width G by A1, MATRIX_0:32;

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

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

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

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

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

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