set D = Deleting (M,i,j);
A3: width M = n by MATRIX_0:24;
len M = n by MATRIX_0:24;
then dom M = Seg n by FINSEQ_1:def 3;
then A4: len (Deleting (M,i,j)) = n -' 1 by A1, Th2;
per cases ( n -' 1 = 0 or n -' 1 > 0 ) ;
suppose n -' 1 = 0 ; :: thesis: Deleting (M,i,j) is Matrix of n -' 1,K
then dom (Deleting (M,i,j)) = Seg 0 by A4, FINSEQ_1:def 3;
then for f being FinSequence of K st f in rng (Deleting (M,i,j)) holds
len f = n -' 1 by RELAT_1:42;
hence Deleting (M,i,j) is Matrix of n -' 1,K by A4, MATRIX_0:def 2; :: thesis: verum
end;
suppose A5: n -' 1 > 0 ; :: thesis: Deleting (M,i,j) is Matrix of n -' 1,K
width (Deleting (M,i,j)) = n -' 1 by A2, A3, Th5;
hence Deleting (M,i,j) is Matrix of n -' 1,K by A4, A5, MATRIX_0:20; :: thesis: verum
end;
end;