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 Th19
.= len (SgmX (RealOrd,(proj2 .: (Values G)))) by Th9 ;
A2: for n, m being 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 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_0:32;
A5: ( 1 <= m & m <= width G ) by A3, MATRIX_0:32;
(SgmX (RealOrd,(proj1 .: (Values G)))) . n = (G * (n,1)) `1 by A4, Th28;
then A6: (SgmX (RealOrd,(proj1 .: (Values G)))) . n = (G * (n,m)) `1 by A4, A5, GOBOARD5:2;
(SgmX (RealOrd,(proj2 .: (Values G)))) . m = (G * (1,m)) `2 by A5, Th29;
then (SgmX (RealOrd,(proj2 .: (Values G)))) . m = (G * (n,m)) `2 by A4, A5, GOBOARD5:1;
hence G * (n,m) = |[((SgmX (RealOrd,(proj1 .: (Values G)))) . n),((SgmX (RealOrd,(proj2 .: (Values G)))) . m)]| by A6, EUCLID:53; :: thesis: verum

end;

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