let n be Nat; :: thesis: for K being Ring
for A being Matrix of n,K holds A * (1. (K,n)) = A
let K be Ring; :: 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: len (1. (K,n)) = n by MATRIX_0:24;
A2: ( width A = n & width (1. (K,n)) = n ) by MATRIX_0:24;
then A3: ( len (A * (1. (K,n))) = len A & width (A * (1. (K,n))) = width (1. (K,n)) ) by A1, Def4;

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

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 A5: [i,j] in Indices (A * (1. (K,n))) ; :: thesis: (A * (1. (K,n))) * (i,j) = A * (i,j)
( dom (A * (1. (K,n))) = Seg (len (A * (1. (K,n)))) & Indices (A * (1. (K,n))) = [:(dom (A * (1. (K,n)))),(Seg (width (A * (1. (K,n))))):] ) by FINSEQ_1:def 3;
A6: ( j in Seg (len (1. (K,n))) & j in Seg (width (1. (K,n))) ) by A1, A2, A3, A5, ZFMISC_1:87;
then j in Seg (len (Col ((1. (K,n)),j))) by MATRIX_0:def 8;
then A7: j in dom (Col ((1. (K,n)),j)) by FINSEQ_1:def 3;
dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def 3;
then j in dom (1. (K,n)) by A6;
then [j,j] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A6, ZFMISC_1:87;
then [j,j] in Indices (1. (K,n)) ;
then A8: (Col ((1. (K,n)),j)) . j = 1. K by Th16;
A9: for k being Nat st k in dom (Col ((1. (K,n)),j)) & k <> j holds
(Col ((1. (K,n)),j)) . k = 0. K

proof

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

end;

j in Seg (len (Line (A,i))) by A2, A6, MATRIX_0:def 7;
then A12: 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 A2, A1, A5, Def4
.= Sum (mlt ((Line (A,i)),(Col ((1. (K,n)),j)))) by FVSUM_1:def 9
.= (Line (A,i)) . j by A7, A12, A9, A8, Th17
.= A * (i,j) by A2, A6, MATRIX_0:def 7 ; :: thesis: verum

end;

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