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:24;
A2: width A = n by MATRIX_1:24;
A3: len (1. (K,n)) = n by MATRIX_1:24;
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 A7: j in Seg (width (1. (K,n))) by A4, ZFMISC_1:87;
then j in Seg (len (Col ((1. (K,n)),j))) by A3, A1, MATRIX_1:def 8;
then A8: j in dom (Col ((1. (K,n)),j)) by FINSEQ_1:def 3;
A9: j in Seg (width A) by A1, A2, A4, A6, ZFMISC_1:87;

A10: 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
A11: k in dom (Col ((1. (K,n)),j)) and
A12: k <> j ; :: thesis: (Col ((1. (K,n)),j)) . k = 0. K
k in Seg (len (Col ((1. (K,n)),j))) by A11, FINSEQ_1:def 3;
then k in Seg (len (1. (K,n))) by MATRIX_1:def 8;
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 A7, ZFMISC_1:87;
then [k,j] in Indices (1. (K,n)) ;
hence (Col ((1. (K,n)),j)) . k = 0. K by A12, Th18; :: thesis: verum

end;

j in dom (1. (K,n)) by A3, A1, A7, FINSEQ_1:def 3;
then [j,j] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A1, A2, A9, ZFMISC_1:87;
then [j,j] in Indices (1. (K,n)) ;
then A13: (Col ((1. (K,n)),j)) . j = 1. K by Th18;
j in Seg (len (Line (A,i))) by A1, A2, A7, MATRIX_1:def 7;
then A14: 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:90
.= Sum (mlt ((Col ((1. (K,n)),j)),(Line (A,i)))) by FVSUM_1:def 9
.= (Line (A,i)) . j by A8, A14, A10, A13, Th19
.= A * (i,j) by A9, MATRIX_1:def 7 ; :: 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