let K be Field; :: thesis: for A being Matrix of 0 ,K holds
( A = {} & A = 1. (K,0) & A = 0. (K,0) )
let A be Matrix of 0 ,K; :: thesis: ( A = {} & A = 1. (K,0) & A = 0. (K,0) )
A1: len A = 0 by MATRIX_0:24;
hence A = {} ; :: thesis: ( A = 1. (K,0) & A = 0. (K,0) )
hence A = 1. (K,0) by Th14; :: thesis: A = 0. (K,0)
thus A = 0. (K,0) by A1; :: thesis: verum