let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n)
let K be Field; :: thesis: for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n)
let M1 be Matrix of n,K; :: thesis: M1 commutes_with 0. (K,n,n)

per cases ( n > 0 or n = 0 ) by NAT_1:3;

suppose A1: n > 0 ; :: thesis: M1 commutes_with 0. (K,n,n)

A2: ( len M1 = n & width M1 = n ) by MATRIX_1:24;
then A3: (0. (K,n,n)) * M1 = 0. (K,n,n) by Th1;
M1 * (0. (K,n,n)) = 0. (K,n,n) by A1, A2, Th2;
hence M1 commutes_with 0. (K,n,n) by A3, Def1; :: thesis: verum

end;

suppose n = 0 ; :: thesis: M1 commutes_with 0. (K,n,n)

then ( len M1 = 0 & len (0. (K,n,n)) = 0 ) by MATRIX_1:def 2;
hence M1 commutes_with 0. (K,n,n) by CARD_2:64; :: thesis: verum

end;

end;