let X be set ; :: thesis: for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
let n, m be Nat; :: thesis: for D being non empty set
for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
let D be non empty set ; :: thesis: for M being Matrix of n,m,D holds M - X is Matrix of n -' (card (M " X)),m,D
let M be Matrix of n,m,D; :: thesis: M - X is Matrix of n -' (card (M " X)),m,D
A1: rng (M - X) c= rng M by FINSEQ_3:66;
rng M c= D * by FINSEQ_1:def 4;
then rng (M - X) c= D * by A1;
then reconsider MX = M - X as FinSequence of D * by FINSEQ_1:def 4;
A2: len MX = (len M) - (card (M " X)) by FINSEQ_3:59;
then len M >= card (M " X) by XREAL_1:49;
then A3: ( len M = n & len MX = (len M) -' (card (M " X)) ) by A2, MATRIX_0:def 2, XREAL_1:233;

per cases ( len MX = 0 or len MX > 0 ) ;

suppose len MX = 0 ; :: thesis: M - X is Matrix of n -' (card (M " X)),m,D

then MX = {} ;
hence M - X is Matrix of n -' (card (M " X)),m,D by A3, MATRIX_0:13; :: thesis: verum

end;

suppose len MX > 0 ; :: thesis: M - X is Matrix of n -' (card (M " X)),m,D

A4: for x being object st x in rng MX holds
ex s being FinSequence st
( s = x & len s = m )

proof

let x be object ; :: thesis: ( x in rng MX implies ex s being FinSequence st
( s = x & len s = m ) )
consider nn being Nat such that
A5: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = nn ) by MATRIX_0:9;
assume A6: x in rng MX ; :: thesis: ex s being FinSequence st
( s = x & len s = m )
then ex p being FinSequence of D st
( x = p & len p = nn ) by A1, A5;
then reconsider p = x as FinSequence of D ;
len p = m by A1, A6, MATRIX_0:def 2;
hence ex s being FinSequence st
( s = x & len s = m ) ; :: thesis: verum

end;

then reconsider MX = MX as Matrix of D by MATRIX_0:def 1;

now :: thesis: for p being FinSequence of D st p in rng MX holds
len p = m

let p be FinSequence of D; :: thesis: ( p in rng MX implies len p = m )
assume p in rng MX ; :: thesis: len p = m
then ex s being FinSequence st
( s = p & len s = m ) by A4;
hence len p = m ; :: thesis: verum

end;

hence M - X is Matrix of n -' (card (M " X)),m,D by A3, MATRIX_0:def 2; :: thesis: verum

end;

end;