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_0:24;
A2: width (1. (K,(len A))) = len A by MATRIX_0:24;
then A3: len ((1. (K,(len A))) * A) = len (1. (K,(len A))) by MATRIX_3:def 4;

A4: now :: thesis: for i, j being Nat st [i,j] in Indices ((1. (K,(len A))) * A) holds
((1. (K,(len A))) * A) * (i,j) = A * (i,j)

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:87;
then i in Seg (len (Line ((1. (K,(len A))),i))) by MATRIX_0:def 7;
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:87;
then [i,i] in Indices (1. (K,(len A))) by A8, ZFMISC_1:87;
then A12: (Line ((1. (K,(len A))),i)) . i = 1_ K by MATRIX_3:15;
i in Seg (len (Col (A,j))) by A2, A8, MATRIX_0:def 8;
then A13: i in dom (Col (A,j)) by FINSEQ_1:def 3;

A14: now :: thesis: for k being Nat st k in dom (Line ((1. (K,(len A))),i)) & k <> i holds
(Line ((1. (K,(len A))),i)) . k = 0. K

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_0:def 7;
then [i,k] in Indices (1. (K,(len A))) by A11, ZFMISC_1:87;
hence (Line ((1. (K,(len A))),i)) . k = 0. K by A16, MATRIX_3:15; :: 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 9
.= (Col (A,j)) . i by A9, A13, A14, A12, MATRIX_3:17
.= A * (i,j) by A1, A5, A10, A11, MATRIX_0:def 8 ; :: 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_0:21; :: thesis: verum