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

Seg (width M) <> {} by A1;
then width M <> {} ;
then len M > 0 by MATRIX_0:def 3;
then A3: len M = 1 by A2, NAT_1:25;
A4: len (Deleting (M,i,j)) = n -' 1 by A2, Th2;
len M = n by MATRIX_0:24;
then len (Deleting (M,i,j)) = 0 by A3, A4, XREAL_1:232;
hence width (Deleting (M,i,j)) = n -' 1 by A4, MATRIX_0:def 3; :: thesis: verum

end;

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

A6: width M = n by MATRIX_0:24;
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_0:24;
DelLine (M,i) = M by A7, FINSEQ_3:104;
hence width (Deleting (M,i,j)) = n -' 1 by A1, A8, Th3; :: thesis: verum

end;

end;