let K be Field; :: thesis: for M being Matrix of K
for k being Nat st k in dom M holds
M . k = Line M,k
let M be Matrix of K; :: 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:27;
then reconsider N = M as Matrix of len M, width M,K by MATRIX_1:20;
k in Seg (len N) by A1, FINSEQ_1:def 3;
hence M . k = Line M,k by Th10; :: thesis: verum