let n be Nat; :: thesis: for K being Ring
for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n)
let K be Ring; :: 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)
A2: ( len M1 = n & width M1 = n ) by MATRIX_0:24;
then (0. (K,n,n)) * M1 = 0. (K,n,n) by Th1;
hence M1 commutes_with 0. (K,n,n) by A2, Th2; :: thesis: verum