let G be Go-board; :: thesis: G = GoB (SgmX RealOrd ,(proj1 .: (Values G))),(SgmX RealOrd ,(proj2 .: (Values G)))
set v1 = SgmX RealOrd ,(proj1 .: (Values G));
set v2 = SgmX RealOrd ,(proj2 .: (Values G));
A1: len G =
card (proj1 .: (Values G))
by Th22
.=
len (SgmX RealOrd ,(proj1 .: (Values G)))
by Th15
;
A2: width G =
card (proj2 .: (Values G))
by Th25
.=
len (SgmX RealOrd ,(proj2 .: (Values G)))
by Th15
;
for n, m being Element of NAT st [n,m] in Indices G holds
G * n,m = |[((SgmX RealOrd ,(proj1 .: (Values G))) . n),((SgmX RealOrd ,(proj2 .: (Values G))) . m)]|
proof
let n,
m be
Element of
NAT ;
:: thesis: ( [n,m] in Indices G implies G * n,m = |[((SgmX RealOrd ,(proj1 .: (Values G))) . n),((SgmX RealOrd ,(proj2 .: (Values G))) . m)]| )
assume A3:
[n,m] in Indices G
;
:: thesis: G * n,m = |[((SgmX RealOrd ,(proj1 .: (Values G))) . n),((SgmX RealOrd ,(proj2 .: (Values G))) . m)]|
then A4:
( 1
<= n &
n <= len G )
by MATRIX_1:39;
then A5:
(SgmX RealOrd ,(proj1 .: (Values G))) . n = (G * n,1) `1
by Th34;
A6:
( 1
<= m &
m <= width G )
by A3, MATRIX_1:39;
then
(SgmX RealOrd ,(proj2 .: (Values G))) . m = (G * 1,m) `2
by Th35;
then A7:
(SgmX RealOrd ,(proj2 .: (Values G))) . m = (G * n,m) `2
by A4, A6, GOBOARD5:2;
(SgmX RealOrd ,(proj1 .: (Values G))) . n = (G * n,m) `1
by A4, A5, A6, GOBOARD5:3;
hence
G * n,
m = |[((SgmX RealOrd ,(proj1 .: (Values G))) . n),((SgmX RealOrd ,(proj2 .: (Values G))) . m)]|
by A7, EUCLID:57;
:: thesis: verum
end;
hence
G = GoB (SgmX RealOrd ,(proj1 .: (Values G))),(SgmX RealOrd ,(proj2 .: (Values G)))
by A1, A2, GOBOARD2:def 1; :: thesis: verum