let K be Field; :: thesis: ( 1. K,0 = 0. K,0 & 1. K,0 = {} )
A1: ( len (1. K,0 ) = 0 & width (1. K,0 ) = 0 ) by MATRIX_1:25;
len (0. K,0 ) = 0 by MATRIX_1:25;
then 0. K,0 = {} ;
hence 1. K,0 = 0. K,0 by A1; :: thesis: 1. K,0 = {}
thus 1. K,0 = {} by A1; :: thesis: verum