let D be non empty set ; :: thesis: for M being Matrix of D
for i being Nat st i in dom M holds
M . i = Line M,i
let M be Matrix of D; :: thesis: for i being Nat st i in dom M holds
M . i = Line M,i
let i be Nat; :: thesis: ( i in dom M implies M . i = Line M,i )
assume A1: i in dom M ; :: thesis: M . i = Line M,i
then A2: M . i in rng M by FUNCT_1:def 5;
rng M c= D * by FINSEQ_1:def 4;
then reconsider p = M . i as FinSequence of D by A2, FINSEQ_1:def 11;
M <> {} by A1, RELAT_1:60;
then M is Matrix of len M, width M,D by MATRIX_1:20;
then A3: len p = width M by A2, MATRIX_1:def 3;
A4: len (Line M,i) = width M by MATRIX_1:def 8;
then A5: dom (Line M,i) = Seg (width M) by FINSEQ_1:def 3;
A6: for j being Nat st j in Seg (width M) holds
M * i,j = p . j

proof

let j be Nat; :: thesis: ( j in Seg (width M) implies M * i,j = p . j )
assume j in Seg (width M) ; :: thesis: M * i,j = p . j
then [i,j] in Indices M by A1, ZFMISC_1:106;
then ex q being FinSequence of D st
( q = M . i & q . j = M * i,j ) by MATRIX_1:def 6;
hence M * i,j = p . j ; :: thesis: verum

end;

now

let j be Nat; :: thesis: ( j in dom (Line M,i) implies (Line M,i) . j = p . j )
assume A7: j in dom (Line M,i) ; :: thesis: (Line M,i) . j = p . j
hence (Line M,i) . j = M * i,j by A5, MATRIX_1:def 8
.= p . j by A6, A5, A7 ;
:: thesis: verum

end;

hence M . i = Line M,i by A3, A4, FINSEQ_2:10; :: thesis: verum