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

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

A6: dom A = Seg (len A) by FINSEQ_1:def 3;
let i, j be Nat; :: thesis: ( [i,j] in Indices ((1. (K,n)) * A) implies ((1. (K,n)) * A) * (i,j) = A * (i,j) )
assume A7: [i,j] in Indices ((1. (K,n)) * A) ; :: thesis: ((1. (K,n)) * A) * (i,j) = A * (i,j)
A8: ( dom ((1. (K,n)) * A) = Seg (len ((1. (K,n)) * A)) & Indices ((1. (K,n)) * A) = [:(dom ((1. (K,n)) * A)),(Seg (width ((1. (K,n)) * A))):] ) by FINSEQ_1:def 3;
then A9: i in Seg (width (1. (K,n))) by A1, A3, A4, A7, ZFMISC_1:87;
then i in Seg (len (Line ((1. (K,n)),i))) by MATRIX_0:def 7;
then A10: i in dom (Line ((1. (K,n)),i)) by FINSEQ_1:def 3;
A11: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def 3;
then A12: i in dom (1. (K,n)) by A4, A7, A8, ZFMISC_1:87;
then [i,i] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A9, ZFMISC_1:87;
then [i,i] in Indices (1. (K,n)) ;
then A13: (Line ((1. (K,n)),i)) . i = 1. K by Th15;

A14: now :: thesis: for k being Nat st k in dom (Line ((1. (K,n)),i)) & k <> i holds
(Line ((1. (K,n)),i)) . k = 0. K

let k be Nat; :: thesis: ( k in dom (Line ((1. (K,n)),i)) & k <> i implies (Line ((1. (K,n)),i)) . k = 0. K )
assume that
A15: k in dom (Line ((1. (K,n)),i)) and
A16: k <> i ; :: thesis: (Line ((1. (K,n)),i)) . k = 0. K
k in Seg (len (Line ((1. (K,n)),i))) by A15, FINSEQ_1:def 3;
then k in Seg (width (1. (K,n))) by MATRIX_0:def 7;
then [i,k] in [:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] by A12, ZFMISC_1:87;
then [i,k] in Indices (1. (K,n)) ;
hence (Line ((1. (K,n)),i)) . k = 0. K by A16, Th15; :: thesis: verum

end;

i in Seg (len (Col (A,j))) by A3, A2, A9, MATRIX_0:def 8;
then A17: i in dom (Col (A,j)) by FINSEQ_1:def 3;
thus ((1. (K,n)) * A) * (i,j) = (Line ((1. (K,n)),i)) "*" (Col (A,j)) by A3, A2, A7, Def4
.= Sum (mlt ((Line ((1. (K,n)),i)),(Col (A,j)))) by FVSUM_1:def 9
.= (Col (A,j)) . i by A10, A17, A14, A13, Th17
.= A * (i,j) by A1, A2, A6, A11, A12, MATRIX_0:def 8 ; :: thesis: verum

end;

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