let n be Nat; :: thesis: for K being Field
for A being Matrix of n,K holds (1. K,n) * A = A
let K be Field; :: 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_1:25;
A2: len A = n by MATRIX_1:25;
A3: width (1. K,n) = n by MATRIX_1:25;
then A4: len ((1. K,n) * A) = len (1. K,n) by A2, Def4;

A5: now

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, MATRIX_1:def 5;
then A9: i in Seg (width (1. K,n)) by A1, A3, A4, A7, ZFMISC_1:106;
then i in Seg (len (Line (1. K,n),i)) by MATRIX_1:def 8;
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:106;
then [i,i] in [:(dom (1. K,n)),(Seg (width (1. K,n))):] by A9, ZFMISC_1:106;
then [i,i] in Indices (1. K,n) by MATRIX_1:def 5;
then A13: (Line (1. K,n),i) . i = 1. K by Th17;

A14: now

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_1:def 8;
then [i,k] in [:(dom (1. K,n)),(Seg (width (1. K,n))):] by A12, ZFMISC_1:106;
then [i,k] in Indices (1. K,n) by MATRIX_1:def 5;
hence (Line (1. K,n),i) . k = 0. K by A16, Th17; :: thesis: verum

end;

i in Seg (len (Col A,j)) by A3, A2, A9, MATRIX_1:def 9;
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 10
.= (Col A,j) . i by A10, A17, A14, A13, Th19
.= A * i,j by A1, A2, A6, A11, A12, MATRIX_1:def 9 ; :: 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_1:21; :: thesis: verum