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 )

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

hence
DelLine (,M) is Matrix of D
by MATRIX_0:9; :: thesis: verum
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;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