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)
then A8: j in Seg (width (1. (K,n))) by A4, 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, 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)) ;
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)) ;
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