let L be Field; :: thesis: for m, n being Nat st m > 0 holds
for M being Matrix of m,n,L holds (1. (L,m)) * M = M
let m, n be Nat; :: thesis: ( m > 0 implies for M being Matrix of m,n,L holds (1. (L,m)) * M = M )
assume A1: m > 0 ; :: thesis: for M being Matrix of m,n,L holds (1. (L,m)) * M = M
let M be Matrix of m,n,L; :: thesis: (1. (L,m)) * M = M
A2: width (1. (L,m)) = m by A1, MATRIX_0:23
.= len M by A1, MATRIX_0:23 ;
set M2 = (1. (L,m)) * M;
A3: len M = m by A1, MATRIX_0:23;
len (1. (L,m)) = m by A1, MATRIX_0:23;
then A4: m = len ((1. (L,m)) * M) by A2, MATRIX_3:def 4;

A5: now :: thesis: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = ((1. (L,m)) * M) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = ((1. (L,m)) * M) * (i,j) )
assume A6: [i,j] in Indices M ; :: thesis: M * (i,j) = ((1. (L,m)) * M) * (i,j)
then A7: i in dom M by ZFMISC_1:87;
dom M = Seg (len M) by FINSEQ_1:def 3
.= dom ((1. (L,m)) * M) by A3, A4, FINSEQ_1:def 3 ;
then Indices M = Indices ((1. (L,m)) * M) by A2, MATRIX_3:def 4;
then A8: ((1. (L,m)) * M) * (i,j) = (Line ((1. (L,m)),i)) "*" (Col (M,j)) by A2, A6, MATRIX_3:def 4
.= Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) by FVSUM_1:def 9 ;
len (Line ((1. (L,m)),i)) = width (1. (L,m)) by MATRIX_0:def 7
.= m by MATRIX_0:24 ;
then A9: dom (Line ((1. (L,m)),i)) = Seg m by FINSEQ_1:def 3;
A10: len M = m by A1, MATRIX_0:23;
then A11: i in dom (Line ((1. (L,m)),i)) by A7, A9, FINSEQ_1:def 3;
A12: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by A1, MATRIX_0:23;
then A13: [i,i] in Indices (1. (L,m)) by A9, A11, ZFMISC_1:87;
A14: for k being Nat st k in dom (Line ((1. (L,m)),i)) & k <> i holds
(Line ((1. (L,m)),i)) . k = 0. L

proof

let k be Nat; :: thesis: ( k in dom (Line ((1. (L,m)),i)) & k <> i implies (Line ((1. (L,m)),i)) . k = 0. L )
assume that
A15: k in dom (Line ((1. (L,m)),i)) and
A16: k <> i ; :: thesis: (Line ((1. (L,m)),i)) . k = 0. L
A17: [i,k] in Indices (1. (L,m)) by A9, A11, A12, A15, ZFMISC_1:87;
k in Seg (width (1. (L,m))) by A9, A15, MATRIX_0:24;
then (Line ((1. (L,m)),i)) . k = (1. (L,m)) * (i,k) by MATRIX_0:def 7
.= 0. L by A16, A17, MATRIX_1:def 3 ;
hence (Line ((1. (L,m)),i)) . k = 0. L ; :: thesis: verum

end;

len (Col (M,j)) = len M by MATRIX_0:def 8
.= m by A1, MATRIX_0:23 ;
then dom (Col (M,j)) = Seg m by FINSEQ_1:def 3;
then A18: i in dom (Col (M,j)) by A7, A10, FINSEQ_1:def 3;
i in Seg (width (1. (L,m))) by A9, A11, MATRIX_0:24;
then A19: (Line ((1. (L,m)),i)) . i = (1. (L,m)) * (i,i) by MATRIX_0:def 7
.= 1. L by A13, MATRIX_1:def 3 ;
i in dom (Line ((1. (L,m)),i)) by A7, A10, A9, FINSEQ_1:def 3;
then Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) = (Col (M,j)) . i by A19, A14, A18, MATRIX_3:17;
hence M * (i,j) = ((1. (L,m)) * M) * (i,j) by A8, A7, MATRIX_0:def 8; :: thesis: verum

end;

width M = width ((1. (L,m)) * M) by A2, MATRIX_3:def 4;
hence (1. (L,m)) * M = M by A3, A4, A5, MATRIX_0:21; :: thesis: verum