let G be Go-board; :: thesis: ( not G is empty & G is non-empty )
thus not G is empty ; :: thesis: G is non-empty
consider n0 being Nat such that
A1: for x being object st x in rng G holds
ex s being FinSequence st
( s = x & len s = n0 ) by MATRIX_0:def 1;
len G <> 0 by MATRIX_0:def 10;
then consider s0 being FinSequence such that
A2: s0 in rng G and
A3: len s0 = width G by MATRIX_0:def 3;
A4: ex s being FinSequence st
( s = s0 & len s = n0 ) by A2, A1;
assume not G is non-empty ; :: thesis: contradiction
then consider n being object such that
A5: n in dom G and
A6: G . n is empty by FUNCT_1:def 9;
A7: card (G . n) is empty by A6;
ex s1 being FinSequence st
( s1 = G . n & len s1 = n0 ) by A5, A1, FUNCT_1:3;
hence contradiction by A3, A4, A7, MATRIX_0:def 10; :: thesis: verum