A1: len (1_Rmatrix 0) = 0 by MATRIX_0:24;
len (0_Rmatrix 0) = 0 by MATRIX_0:24;
then 0_Rmatrix 0 = {} ;
hence 1_Rmatrix 0 = 0_Rmatrix 0 by A1; :: thesis: 1_Rmatrix 0 = {}
thus 1_Rmatrix 0 = {} by A1; :: thesis: verum