let K be Field; :: thesis: for A being Matrix of K holds (1. K,(len A)) * A = A
let A be Matrix of K; :: thesis: (1. K,(len A)) * A = A
set n = len A;
set B = 1. K,(len A);
A1: ( len (1. K,(len A)) = len A & width (1. K,(len A)) = len A & len A = len A ) by MATRIX_1:25;
then A2: ( len ((1. K,(len A)) * A) = len (1. K,(len A)) & width ((1. K,(len A)) * A) = width A ) by MATRIX_3:def 4;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((1. K,(len A)) * A) implies ((1. K,(len A)) * A) * i,j = A * i,j )
assume A3: [i,j] in Indices ((1. K,(len A)) * A) ; :: thesis: ((1. K,(len A)) * A) * i,j = A * i,j
A4: ( dom A = Seg (len A) & dom (1. K,(len A)) = Seg (len (1. K,(len A))) & dom ((1. K,(len A)) * A) = Seg (len ((1. K,(len A)) * A)) ) by FINSEQ_1:def 3;
then A5: ( i in dom (1. K,(len A)) & i in Seg (width (1. K,(len A))) ) by A1, A2, A3, ZFMISC_1:106;
then A6: [i,i] in Indices (1. K,(len A)) by ZFMISC_1:106;
i in Seg (len (Line (1. K,(len A)),i)) by A5, MATRIX_1:def 8;
then A7: i in dom (Line (1. K,(len A)),i) by FINSEQ_1:def 3;
i in Seg (len (Col A,j)) by A1, A5, MATRIX_1:def 9;
then A8: i in dom (Col A,j) by FINSEQ_1:def 3;
A9: ( (Line (1. K,(len A)),i) . i = 1_ K & ( for k being Nat st k in dom (Line (1. K,(len A)),i) & k <> i holds
(Line (1. K,(len A)),i) . k = 0. K ) )

proof

thus (Line (1. K,(len A)),i) . i = 1_ K by A6, MATRIX_3:17; :: thesis: for k being Nat st k in dom (Line (1. K,(len A)),i) & k <> i holds
(Line (1. K,(len A)),i) . k = 0. K

now

let k be Nat; :: thesis: ( k in dom (Line (1. K,(len A)),i) & k <> i implies (Line (1. K,(len A)),i) . k = 0. K )
assume A10: ( k in dom (Line (1. K,(len A)),i) & k <> i ) ; :: thesis: (Line (1. K,(len A)),i) . k = 0. K
then k in Seg (len (Line (1. K,(len A)),i)) by FINSEQ_1:def 3;
then k in Seg (width (1. K,(len A))) by MATRIX_1:def 8;
then [i,k] in Indices (1. K,(len A)) by A5, ZFMISC_1:106;
hence (Line (1. K,(len A)),i) . k = 0. K by A10, MATRIX_3:17; :: thesis: verum

end;

hence for k being Nat st k in dom (Line (1. K,(len A)),i) & k <> i holds
(Line (1. K,(len A)),i) . k = 0. K ; :: thesis: verum

end;

thus ((1. K,(len A)) * A) * i,j = (Line (1. K,(len A)),i) "*" (Col A,j) by A1, A3, MATRIX_3:def 4
.= Sum (mlt (Line (1. K,(len A)),i),(Col A,j)) by FVSUM_1:def 10
.= (Col A,j) . i by A7, A8, A9, MATRIX_3:19
.= A * i,j by A1, A4, A5, MATRIX_1:def 9 ; :: thesis: verum

end;

hence (1. K,(len A)) * A = A by A1, A2, MATRIX_1:21; :: thesis: verum