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 3;
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;
then M is Matrix of len M, width M,D by Th20;
then A3: len p = width M by A2, Def2;
A4: len (Line (M,i)) = width M by Def7;
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:87;
then ex q being FinSequence of D st
( q = M . i & q . j = M * (i,j) ) by Def5;
hence M * (i,j) = p . j ; :: thesis: verum

end;

now :: thesis: for j being Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j = p . j

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, Def7
.= p . j by A6, A5, A7 ;
:: thesis: verum

end;

hence M . i = Line (M,i) by A3, A4, FINSEQ_2:9; :: thesis: verum