let G be Go-board; 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;
( [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
;
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;
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; verum