let D be non empty set ; :: thesis: for M being Matrix of D
for k being Nat st k in dom M holds
M . k = Line (M,k)
let M be Matrix of D; :: thesis: for k being Nat st k in dom M holds
M . k = Line (M,k)
let k be Nat; :: thesis: ( k in dom M implies M . k = Line (M,k) )
assume A1: k in dom M ; :: thesis: M . k = Line (M,k)
then ( 1 <= k & k <= len M ) by FINSEQ_3:25;
then reconsider N = M as Matrix of len M, width M,D by Th20;
k in Seg (len N) by A1, FINSEQ_1:def 3;
hence M . k = Line (M,k) by Th52; :: thesis: verum