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: ( len ((1_ K) * M) = len M & width ((1_ K) * M) = width M ) by MATRIX_3:def 5;
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 )
assume A2: [i,j] in Indices M ; :: thesis: ((1_ K) * M) * i,j = M * i,j
(1_ K) * (M * i,j) = M * i,j by VECTSP_1:def 19;
hence ((1_ K) * M) * i,j = M * i,j by A2, MATRIX_3:def 5; :: thesis: verum

end;

hence (1_ K) * M = M by A1, MATRIX_1:21; :: thesis: verum