consider n being Nat such that
A1: for x being object st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by Def1;
take n ; :: according to MATRIX_0:def 1 :: thesis: for x being object st x in rng (DelLine (,M)) holds
ex s being FinSequence st
( s = x & len s = n )
let x be object ; :: thesis: ( x in rng (DelLine (,M)) implies ex s being FinSequence st
( s = x & len s = n ) )
A2: rng (DelLine (,M)) c= rng M by FINSEQ_3:106;
assume x in rng (DelLine (,M)) ; :: thesis: ex s being FinSequence st
( s = x & len s = n )
hence ex s being FinSequence st
( s = x & len s = n ) by A1, A2; :: thesis: verum