let n be Nat; for K being Field
for M being Matrix of n,K st n > 0 holds
M * (0. (K,n,n)) = 0. (K,n,n)
let K be Field; for M being Matrix of n,K st n > 0 holds
M * (0. (K,n,n)) = 0. (K,n,n)
let M be Matrix of n,K; ( n > 0 implies M * (0. (K,n,n)) = 0. (K,n,n) )
assume A1:
n > 0
; M * (0. (K,n,n)) = 0. (K,n,n)
A2:
( len (0. (K,n,n)) = len (0. (K,n,n)) & width (0. (K,n,n)) = width (0. (K,n,n)) )
;
A3:
( len M = n & width M = n & len (0. (K,n,n)) = n )
by MATRIX_0:24;
reconsider M0 = M * (0. (K,n,n)) as Matrix of K ;
A4:
( len M0 = n & width M0 = n )
by MATRIX_0:24;
M * (0. (K,n,n)) =
M * ((0. (K,n,n)) + (0. (K,n,n)))
by MATRIX_3:4
.=
(M * (0. (K,n,n))) + (M * (0. (K,n,n)))
by A2, A3, A1, MATRIX_4:62
;
hence
M * (0. (K,n,n)) = 0. (K,n,n)
by A4, MATRIX_4:6; verum