A1: ( len (1_Rmatrix 0 ) = 0 & width (1_Rmatrix 0 ) = 0 ) by MATRIX_1:25;
( len (0_Rmatrix 0 ) = 0 & width (0_Rmatrix 0 ) = 0 ) by MATRIX_1:25;
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