A1: width M <> 0 by GOBOARD1:def 3;
then width (M @) = len M by MATRIX_2:10;
then A2: width (M @) <> 0 by GOBOARD1:def 3;
len (M @) <> 0 by A1, MATRIX_2:10;
hence not M @ is empty-yielding by A2, GOBOARD1:def 3; :: thesis: verum