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