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_1:25;
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