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
( len M = n & dom M = Seg (len M) ) by FINSEQ_1:def 3, MATRIX_1:26;
then A2: M . k in rng M by A1, 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 A3: 0 < n ; :: thesis: M . k = Line M,k

consider l being Nat such that
A4: 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
A5: M . k = p and
len p = l by A2, A4;
A6: width M = m by A3, MATRIX_1:24;
A7: 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, A6, ZFMISC_1:106;
then [k,j] in Indices M by A3, 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 A5; :: thesis: verum

end;

len p = width M by A2, A6, A5, MATRIX_1:def 3;
hence M . k = Line M,k by A5, A7, MATRIX_1:def 8; :: thesis: verum

end;

end;