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)

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;

end;

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;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

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