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

A4: now

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:106;
then j in Seg (len (Line A,i)) by A1, MATRIX_1:def 8;
then A7: j in dom (Line A,i) by FINSEQ_1:def 3;

A8: now

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_1:def 9;
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:106;
hence (Col (1. K,(width A)),j) . k = 0. K by A10, MATRIX_3:18; :: thesis: verum

end;

A11: j in Seg (width A) by A1, A3, A5, ZFMISC_1:106;
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:106;
then A12: (Col (1. K,(width A)),j) . j = 1_ K by MATRIX_3:18;
j in Seg (len (Col (1. K,(width A)),j)) by A2, A1, A6, MATRIX_1:def 9;
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:115
.= Sum (mlt (Col (1. K,(width A)),j),(Line A,i)) by FVSUM_1:def 10
.= (Line A,i) . j by A13, A7, A8, A12, MATRIX_3:19
.= A * i,j by A11, MATRIX_1:def 8 ; :: 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_1:21; :: thesis: verum