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_1:24
.= len M by A1, MATRIX_1:24 ;
set M2 = (1. L,m) * M;
A3: len M = m by A1, MATRIX_1:24;
len (1. L,m) = m by A1, MATRIX_1:24;
then A4: m = len ((1. L,m) * M) by A2, MATRIX_3:def 4;

A5: now

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:106;
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 10 ;
len (Line (1. L,m),i) = width (1. L,m) by MATRIX_1:def 8
.= m by MATRIX_1:25 ;
then A9: dom (Line (1. L,m),i) = Seg m by FINSEQ_1:def 3;
A10: len M = m by A1, MATRIX_1:24;
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_1:24;
then A13: [i,i] in Indices (1. L,m) by A9, A11, ZFMISC_1:106;
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:106;
k in Seg (width (1. L,m)) by A9, A15, MATRIX_1:25;
then (Line (1. L,m),i) . k = (1. L,m) * i,k by MATRIX_1:def 8
.= 0. L by A16, A17, MATRIX_1:def 12 ;
hence (Line (1. L,m),i) . k = 0. L ; :: thesis: verum

end;

len (Col M,j) = len M by MATRIX_1:def 9
.= m by A1, MATRIX_1:24 ;
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_1:25;
then A19: (Line (1. L,m),i) . i = (1. L,m) * i,i by MATRIX_1:def 8
.= 1. L by A13, MATRIX_1:def 12 ;
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:19;
hence M * i,j = ((1. L,m) * M) * i,j by A8, A7, MATRIX_1:def 9; :: 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_1:21; :: thesis: verum