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 Th25, FINSEQ_1:def 3;
then A2: M . k in rng M by A1, FUNCT_1:def 3;

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 object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = l ) by Th9;
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, Th23;
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:87;
then [k,j] in Indices M by A3, Th23;
then ex q being FinSequence of D st
( q = M . k & M * (k,j) = q . j ) by Def5;
hence p . j = M * (k,j) by A5; :: thesis: verum

end;

len p = width M by A2, A6, A5, Def2;
hence M . k = Line (M,k) by A5, A7, Def7; :: thesis: verum

end;

end;