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 set st x in rng G holds
ex s being FinSequence st
( s = x & len s = n0 ) by MATRIX_1:def 1;
len G <> 0 by GOBOARD1:def 5;
then consider s0 being FinSequence such that
A2: s0 in rng G and
A3: len s0 = width G by MATRIX_1:def 4;
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 set such that
A5: n in dom G and
A6: G . n is empty by FUNCT_1:def 15;
ex s1 being FinSequence st
( s1 = G . n & len s1 = n0 ) by A5, A1, FUNCT_1:12;
hence contradiction by A6, A3, A4, CARD_1:47, GOBOARD1:def 5; :: thesis: verum