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;

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 )
;

end;

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;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