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)

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

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

( len ((1_ K) * M) = len M & width ((1_ K) * M) = width M )
by MATRIX_3:def 5;
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;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

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