let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds
G = GoB f
let G be Go-board; :: thesis: ( proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) implies G = GoB f )
X_axis f = proj1 * f by Th10;
then rng (X_axis f) = proj1 .: (rng f) by RELAT_1:127;
then A1: Incr (X_axis f) = SgmX (RealOrd,(proj1 .: (rng f))) by Th8;
Y_axis f = proj2 * f by Th11;
then rng (Y_axis f) = proj2 .: (rng f) by RELAT_1:127;
then A2: Incr (Y_axis f) = SgmX (RealOrd,(proj2 .: (rng f))) by Th8;
assume ( proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) ) ; :: thesis: G = GoB f
hence G = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A1, A2, Th32
.= GoB f by GOBOARD2:def 2 ;
:: thesis: verum