let K be Field; :: thesis: for A being Matrix of K holds (1. K,(len A)) * A = A
let A be Matrix of K; :: thesis: (1. K,(len A)) * A = A
set n = len A;
set B = 1. K,(len A);
A1: len (1. K,(len A)) = len A by MATRIX_1:25;
A2: width (1. K,(len A)) = len A by MATRIX_1:25;
then A3: len ((1. K,(len A)) * A) = len (1. K,(len A)) by MATRIX_3:def 4;

A4: now

A5: dom A = Seg (len A) by FINSEQ_1:def 3;
let i, j be Nat; :: thesis: ( [i,j] in Indices ((1. K,(len A)) * A) implies ((1. K,(len A)) * A) * i,j = A * i,j )
assume A6: [i,j] in Indices ((1. K,(len A)) * A) ; :: thesis: ((1. K,(len A)) * A) * i,j = A * i,j
A7: dom ((1. K,(len A)) * A) = Seg (len ((1. K,(len A)) * A)) by FINSEQ_1:def 3;
then A8: i in Seg (width (1. K,(len A))) by A1, A2, A3, A6, ZFMISC_1:106;
then i in Seg (len (Line (1. K,(len A)),i)) by MATRIX_1:def 8;
then A9: i in dom (Line (1. K,(len A)),i) by FINSEQ_1:def 3;
A10: dom (1. K,(len A)) = Seg (len (1. K,(len A))) by FINSEQ_1:def 3;
then A11: i in dom (1. K,(len A)) by A3, A6, A7, ZFMISC_1:106;
then [i,i] in Indices (1. K,(len A)) by A8, ZFMISC_1:106;
then A12: (Line (1. K,(len A)),i) . i = 1_ K by MATRIX_3:17;
i in Seg (len (Col A,j)) by A2, A8, MATRIX_1:def 9;
then A13: i in dom (Col A,j) by FINSEQ_1:def 3;

A14: now

let k be Nat; :: thesis: ( k in dom (Line (1. K,(len A)),i) & k <> i implies (Line (1. K,(len A)),i) . k = 0. K )
assume that
A15: k in dom (Line (1. K,(len A)),i) and
A16: k <> i ; :: thesis: (Line (1. K,(len A)),i) . k = 0. K
k in Seg (len (Line (1. K,(len A)),i)) by A15, FINSEQ_1:def 3;
then k in Seg (width (1. K,(len A))) by MATRIX_1:def 8;
then [i,k] in Indices (1. K,(len A)) by A11, ZFMISC_1:106;
hence (Line (1. K,(len A)),i) . k = 0. K by A16, MATRIX_3:17; :: thesis: verum

end;

thus ((1. K,(len A)) * A) * i,j = (Line (1. K,(len A)),i) "*" (Col A,j) by A2, A6, MATRIX_3:def 4
.= Sum (mlt (Line (1. K,(len A)),i),(Col A,j)) by FVSUM_1:def 10
.= (Col A,j) . i by A9, A13, A14, A12, MATRIX_3:19
.= A * i,j by A1, A5, A10, A11, MATRIX_1:def 9 ; :: thesis: verum

end;

width ((1. K,(len A)) * A) = width A by A2, MATRIX_3:def 4;
hence (1. K,(len A)) * A = A by A1, A3, A4, MATRIX_1:21; :: thesis: verum