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 )
len A = 0 by MATRIX_1:25;
hence A = {} ; :: thesis: ( A = 1. K,0 & A = 0. K,0 )
hence A = 1. K,0 by MR103; :: thesis: A = 0. K,0
hence A = 0. K,0 by MR103; :: thesis: verum