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: width G = card (proj2 .: (Values G)) by Th25
.= len (SgmX RealOrd ,(proj2 .: (Values G))) by Th15 ;
A2: 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;
A5: ( 1 <= m & m <= width G ) by A3, MATRIX_1:39;
(SgmX RealOrd ,(proj1 .: (Values G))) . n = (G * n,1) `1 by A4, Th34;
then A6: (SgmX RealOrd ,(proj1 .: (Values G))) . n = (G * n,m) `1 by A4, A5, GOBOARD5:3;
(SgmX RealOrd ,(proj2 .: (Values G))) . m = (G * 1,m) `2 by A5, Th35;
then (SgmX RealOrd ,(proj2 .: (Values G))) . m = (G * n,m) `2 by A4, A5, GOBOARD5:2;
hence G * n,m = |[((SgmX RealOrd ,(proj1 .: (Values G))) . n),((SgmX RealOrd ,(proj2 .: (Values G))) . m)]| by A6, EUCLID:57; :: thesis: verum

end;

len G = card (proj1 .: (Values G)) by Th22
.= len (SgmX RealOrd ,(proj1 .: (Values G))) by Th15 ;
hence G = GoB (SgmX RealOrd ,(proj1 .: (Values G))),(SgmX RealOrd ,(proj2 .: (Values G))) by A1, A2, GOBOARD2:def 1; :: thesis: verum