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