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