let K be Field; :: thesis: for M being Matrix of K holds (1_ K) * M = M
let M be Matrix of K; :: thesis: (1_ K) * M = M
A1: for i, j being Nat st [i,j] in Indices M holds
((1_ K) * M) * i,j = M * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies ((1_ K) * M) * i,j = M * i,j )
A2: (1_ K) * (M * i,j) = M * i,j by VECTSP_1:def 19;
assume [i,j] in Indices M ; :: thesis: ((1_ K) * M) * i,j = M * i,j
hence ((1_ K) * M) * i,j = M * i,j by A2, MATRIX_3:def 5; :: thesis: verum

end;

( len ((1_ K) * M) = len M & width ((1_ K) * M) = width M ) by MATRIX_3:def 5;
hence (1_ K) * M = M by A1, MATRIX_1:21; :: thesis: verum