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_0: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; :: 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_0:def 2;
hence M1 commutes_with 0. (K,n,n) by CARD_2:64; :: thesis: verum
end;
end;