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

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

let i, j be Nat; :: thesis: ( [i,j] in Indices (A * (1. (K,(width A)))) implies (A * (1. (K,(width A)))) * (i,j) = A * (i,j) )
assume A5: [i,j] in Indices (A * (1. (K,(width A)))) ; :: thesis: (A * (1. (K,(width A)))) * (i,j) = A * (i,j)
then A6: j in Seg (width (1. (K,(width A)))) by A3, ZFMISC_1:87;
then j in Seg (len (Line (A,i))) by A1, MATRIX_0:def 7;
then A7: j in dom (Line (A,i)) by FINSEQ_1:def 3;

A8: now :: thesis: for k being Nat st k in dom (Col ((1. (K,(width A))),j)) & k <> j holds
(Col ((1. (K,(width A))),j)) . k = 0. K

let k be Nat; :: thesis: ( k in dom (Col ((1. (K,(width A))),j)) & k <> j implies (Col ((1. (K,(width A))),j)) . k = 0. K )
assume that
A9: k in dom (Col ((1. (K,(width A))),j)) and
A10: k <> j ; :: thesis: (Col ((1. (K,(width A))),j)) . k = 0. K
k in Seg (len (Col ((1. (K,(width A))),j))) by A9, FINSEQ_1:def 3;
then k in Seg (len (1. (K,(width A)))) by MATRIX_0:def 8;
then k in dom (1. (K,(width A))) by FINSEQ_1:def 3;
then [k,j] in Indices (1. (K,(width A))) by A6, ZFMISC_1:87;
hence (Col ((1. (K,(width A))),j)) . k = 0. K by A10, MATRIX_3:16; :: thesis: verum

end;

A11: j in Seg (width A) by A1, A3, A5, ZFMISC_1:87;
then j in dom (1. (K,(width A))) by A2, FINSEQ_1:def 3;
then [j,j] in Indices (1. (K,(width A))) by A1, A11, ZFMISC_1:87;
then A12: (Col ((1. (K,(width A))),j)) . j = 1_ K by MATRIX_3:16;
j in Seg (len (Col ((1. (K,(width A))),j))) by A2, A1, A6, MATRIX_0:def 8;
then A13: j in dom (Col ((1. (K,(width A))),j)) by FINSEQ_1:def 3;
thus (A * (1. (K,(width A)))) * (i,j) = (Line (A,i)) "*" (Col ((1. (K,(width A))),j)) by A2, A5, MATRIX_3:def 4
.= (Col ((1. (K,(width A))),j)) "*" (Line (A,i)) by FVSUM_1:90
.= Sum (mlt ((Col ((1. (K,(width A))),j)),(Line (A,i)))) by FVSUM_1:def 9
.= (Line (A,i)) . j by A13, A7, A8, A12, MATRIX_3:17
.= A * (i,j) by A11, MATRIX_0:def 7 ; :: thesis: verum

end;

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