let R be Ring; :: thesis: for n being Nat
for r being Element of R holds r * (0. (R,n)) = 0. (R,n)
let n be Nat; :: thesis: for r being Element of R holds r * (0. (R,n)) = 0. (R,n)
let r be Element of R; :: thesis: r * (0. (R,n)) = 0. (R,n)
for i, j being Nat st [i,j] in Indices (0. (R,n)) holds
(r * (0. (R,n))) * (i,j) = (0. (R,n)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (0. (R,n)) implies (r * (0. (R,n))) * (i,j) = (0. (R,n)) * (i,j) )
assume A1: [i,j] in Indices (0. (R,n)) ; :: thesis: (r * (0. (R,n))) * (i,j) = (0. (R,n)) * (i,j)
hence (r * (0. (R,n))) * (i,j) = r * ((0. (R,n)) * (i,j)) by MATRIX_3:def 5
.= r * (0. R) by A1, MATRIX_1:1
.= (0. (R,n)) * (i,j) by A1, MATRIX_1:1 ;
:: thesis: verum

end;

hence r * (0. (R,n)) = 0. (R,n) by MATRIX_0:27; :: thesis: verum