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 )

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:
let x be object ; :: thesis:
assume A2: x in rng (Del (M,k)) ; :: thesis:
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:
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:

end;