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