let i, j be Nat; for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = (1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))
let G be Go-board; ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G implies (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = (1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j))) )
assume that
A1:
1 <= i
and
A2:
i + 1 <= len G
and
A3:
1 <= j
and
A4:
j + 1 <= width G
; (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = (1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))
A5:
j < width G
by A4, NAT_1:13;
A6:
1 <= j + 1
by NAT_1:11;
A7:
1 <= i + 1
by NAT_1:11;
then A8: (G * ((i + 1),j)) `1 =
(G * ((i + 1),1)) `1
by A2, A3, A5, GOBOARD5:2
.=
(G * ((i + 1),(j + 1))) `1
by A2, A4, A7, A6, GOBOARD5:2
;
A9:
i < len G
by A2, NAT_1:13;
then A10: (G * (i,j)) `1 =
(G * (i,1)) `1
by A1, A3, A5, GOBOARD5:2
.=
(G * (i,(j + 1))) `1
by A1, A4, A9, A6, GOBOARD5:2
;
A11: (G * ((i + 1),(j + 1))) `2 =
(G * (1,(j + 1))) `2
by A2, A4, A7, A6, GOBOARD5:1
.=
(G * (i,(j + 1))) `2
by A1, A4, A9, A6, GOBOARD5:1
;
A12: (G * (i,j)) `2 =
(G * (1,j)) `2
by A1, A3, A9, A5, GOBOARD5:1
.=
(G * ((i + 1),j)) `2
by A2, A3, A7, A5, GOBOARD5:1
;
A13: ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `2 =
(1 / 2) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `2)
by TOPREAL3:4
.=
(1 / 2) * (((G * (i,j)) `2) + ((G * ((i + 1),(j + 1))) `2))
by TOPREAL3:2
.=
(1 / 2) * (((G * (i,(j + 1))) + (G * ((i + 1),j))) `2)
by A12, A11, TOPREAL3:2
.=
((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))) `2
by TOPREAL3:4
;
((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 =
(1 / 2) * (((G * (i,j)) + (G * ((i + 1),(j + 1)))) `1)
by TOPREAL3:4
.=
(1 / 2) * (((G * (i,j)) `1) + ((G * ((i + 1),(j + 1))) `1))
by TOPREAL3:2
.=
(1 / 2) * (((G * (i,(j + 1))) + (G * ((i + 1),j))) `1)
by A10, A8, TOPREAL3:2
.=
((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))) `1
by TOPREAL3:4
;
hence (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) =
|[(((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))) `1),(((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))) `2)]|
by A13, EUCLID:53
.=
(1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),j)))
by EUCLID:53
;
verum