let n, m be Nat; :: thesis: for D being non empty set
for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line M,k
let D be non empty set ; :: thesis: for M being Matrix of n,m,D
for k being Nat st k in Seg n holds
M . k = Line M,k
let M be Matrix of n,m,D; :: thesis: for k being Nat st k in Seg n holds
M . k = Line M,k
let k be Nat; :: thesis: ( k in Seg n implies M . k = Line M,k )
assume A1: k in Seg n ; :: thesis: M . k = Line M,k
A2: len M = n by MATRIX_1:26;
dom M = Seg (len M) by FINSEQ_1:def 3;
then A3: M . k in rng M by A1, A2, FUNCT_1:def 5;

per cases ( n = 0 or 0 < n ) ;

suppose n = 0 ; :: thesis: M . k = Line M,k

hence M . k = Line M,k by A1; :: thesis: verum

end;

suppose A4: 0 < n ; :: thesis: M . k = Line M,k

then A5: width M = m by MATRIX_1:24;
consider l being Nat such that
A6: for x being set st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = l ) by MATRIX_1:9;
consider p being FinSequence of D such that
A7: M . k = p and
len p = l by A3, A6;
A8: len p = width M by A3, A5, A7, MATRIX_1:def 3;
for j being Nat st j in Seg (width M) holds
p . j = M * k,j

proof

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

end;

hence M . k = Line M,k by A7, A8, MATRIX_1:def 8; :: thesis: verum

end;

end;