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

A5: now

let i, j be Nat; :: thesis: ( [i,j] in Indices (A * (1. K,n)) implies (A * (1. K,n)) * i,j = A * i,j )
assume A6: [i,j] in Indices (A * (1. K,n)) ; :: thesis: (A * (1. K,n)) * i,j = A * i,j
A7: Indices (A * (1. K,n)) = [:(dom (A * (1. K,n))),(Seg (width (A * (1. K,n)))):] by MATRIX_1:def 5;
then A8: j in Seg (width (1. K,n)) by A4, A6, ZFMISC_1:106;
then j in Seg (len (Col (1. K,n),j)) by A3, A1, MATRIX_1:def 9;
then A9: j in dom (Col (1. K,n),j) by FINSEQ_1:def 3;
A10: j in Seg (width A) by A1, A2, A4, A6, A7, ZFMISC_1:106;

A11: now

let k be Nat; :: thesis: ( k in dom (Col (1. K,n),j) & k <> j implies (Col (1. K,n),j) . k = 0. K )
assume that
A12: k in dom (Col (1. K,n),j) and
A13: k <> j ; :: thesis: (Col (1. K,n),j) . k = 0. K
k in Seg (len (Col (1. K,n),j)) by A12, FINSEQ_1:def 3;
then k in Seg (len (1. K,n)) by MATRIX_1:def 9;
then k in dom (1. K,n) by FINSEQ_1:def 3;
then [k,j] in [:(dom (1. K,n)),(Seg (width (1. K,n))):] by A8, ZFMISC_1:106;
then [k,j] in Indices (1. K,n) by MATRIX_1:def 5;
hence (Col (1. K,n),j) . k = 0. K by A13, Th18; :: thesis: verum

end;

j in dom (1. K,n) by A3, A1, A8, FINSEQ_1:def 3;
then [j,j] in [:(dom (1. K,n)),(Seg (width (1. K,n))):] by A1, A2, A10, ZFMISC_1:106;
then [j,j] in Indices (1. K,n) by MATRIX_1:def 5;
then A14: (Col (1. K,n),j) . j = 1. K by Th18;
j in Seg (len (Line A,i)) by A1, A2, A8, MATRIX_1:def 8;
then A15: j in dom (Line A,i) by FINSEQ_1:def 3;
thus (A * (1. K,n)) * i,j = (Line A,i) "*" (Col (1. K,n),j) by A3, A2, A6, Def4
.= (Col (1. K,n),j) "*" (Line A,i) by FVSUM_1:115
.= Sum (mlt (Col (1. K,n),j),(Line A,i)) by FVSUM_1:def 10
.= (Line A,i) . j by A9, A15, A11, A14, Th19
.= A * i,j by A10, MATRIX_1:def 8 ; :: thesis: verum

end;

len (A * (1. K,n)) = len A by A3, A2, Def4;
hence A * (1. K,n) = A by A1, A2, A4, A5, MATRIX_1:21; :: thesis: verum