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