let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( n > 0 implies M * (0. (K,n,n)) = 0. (K,n,n) )
assume A1: n > 0 ; :: thesis: 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; :: thesis: verum