set D = Deleting M,i,j;
A3: ( len M = n & width M = n ) by MATRIX_1:25;
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 & Seg 0 = {} ) by A4, FINSEQ_1:4, 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:65;
hence Deleting M,i,j is Matrix of n -' 1,K by A4, MATRIX_1:def 3; :: 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_1:20; :: thesis: verum

end;

end;