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:25;
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 FINSEQ_1:def 18, MATRIX_1:def 3;
hence M1 commutes_with 0. K,n,n by CARD_2:83; :: thesis: verum

end;

end;