let j, n be Nat; :: thesis: for K being Field
for M being Matrix of n,K
for i being Nat st j in Seg (width M) holds
width (Deleting M,i,j) = n -' 1
let K be Field; :: thesis: for M being Matrix of n,K
for i being Nat st j in Seg (width M) holds
width (Deleting M,i,j) = n -' 1
let M be Matrix of n,K; :: thesis: for i being Nat st j in Seg (width M) holds
width (Deleting M,i,j) = n -' 1
let i be Nat; :: thesis: ( j in Seg (width M) implies width (Deleting M,i,j) = n -' 1 )
assume A1: j in Seg (width M) ; :: thesis: width (Deleting M,i,j) = n -' 1

per cases ( ( len M <= 1 & i in dom M ) or len M > 1 or not i in dom M ) ;

suppose A2: ( len M <= 1 & i in dom M ) ; :: thesis: width (Deleting M,i,j) = n -' 1

len M > 0 by A1, FINSEQ_1:4, MATRIX_1:def 4;
then A3: ( len M = 1 & len M = n & len (Deleting M,i,j) = n -' 1 ) by A2, Th2, MATRIX_1:25, NAT_1:26;
then len (Deleting M,i,j) = 0 by XREAL_1:234;
hence width (Deleting M,i,j) = n -' 1 by A3, MATRIX_1:def 4; :: thesis: verum

end;

suppose len M > 1 ; :: thesis: width (Deleting M,i,j) = n -' 1

then ( width M = width (DelLine M,i) & width M = n ) by Th4, MATRIX_1:25;
hence width (Deleting M,i,j) = n -' 1 by A1, Th3; :: thesis: verum

end;

suppose not i in dom M ; :: thesis: width (Deleting M,i,j) = n -' 1

then ( DelLine M,i = M & width M = n ) by FINSEQ_3:113, MATRIX_1:25;
hence width (Deleting M,i,j) = n -' 1 by A1, Th3; :: thesis: verum

end;

end;