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

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

end;

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

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

end;

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

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

end;

end;