ex n being Nat st
for x being object st x in rng (Del (M,k)) holds
ex p being FinSequence of D st
( x = p & len p = n )

proof

consider n being Nat such that
A1: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = n ) by MATRIX_0:9;
take n ; :: thesis: for x being object st x in rng (Del (M,k)) holds
ex p being FinSequence of D st
( x = p & len p = n )
let x be object ; :: thesis: ( x in rng (Del (M,k)) implies ex p being FinSequence of D st
( x = p & len p = n ) )
assume A2: x in rng (Del (M,k)) ; :: thesis: ex p being FinSequence of D st
( x = p & len p = n )
Del (M,k) is FinSequence of D * by FINSEQ_3:105;
then rng (Del (M,k)) c= D * by FINSEQ_1:def 4;
then reconsider p = x as FinSequence of D by A2, FINSEQ_1:def 11;
take p ; :: thesis: ( x = p & len p = n )
rng (Del (M,k)) c= rng M by FINSEQ_3:106;
then ex p1 being FinSequence of D st
( x = p1 & len p1 = n ) by A1, A2;
hence ( x = p & len p = n ) ; :: thesis: verum

end;

hence DelLine (,M) is Matrix of D by MATRIX_0:9; :: thesis: verum