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) ;
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_0:21; :: thesis: verum