consider n being Nat such that
A1: for x being set st x in rng M holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_1:def 1;
take n ; :: according to MATRIX_1:def 1 :: thesis: for b₁ being set holds
( not b₁ in proj2 (DelLine (,M)) or ex b₂ being set st
( b₂ = b₁ & len b₂ = n ) )
let x be set ; :: thesis: ( not x in proj2 (DelLine (,M)) or ex b₁ being set st
( b₁ = x & len b₁ = n ) )
A2: rng (DelLine (,M)) c= rng M by FINSEQ_3:106;
assume x in rng (DelLine (,M)) ; :: thesis: ex b₁ being set st
( b₁ = x & len b₁ = n )
hence ex b₁ being set st
( b₁ = x & len b₁ = n ) by A1, A2; :: thesis: verum