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 () 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 () holds
width (Deleting (M,i,j)) = n -' 1

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

let i be Nat; :: thesis: ( j in Seg () implies width (Deleting (M,i,j)) = n -' 1 )
assume A1: j in Seg () ; :: 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 () <> {} by A1;
then width M <> {} ;
then len M > 0 by MATRIX_0:def 3;
then A3: len M = 1 by ;
A4: len (Deleting (M,i,j)) = n -' 1 by ;
len M = n by MATRIX_0:24;
then len (Deleting (M,i,j)) = 0 by ;
hence width (Deleting (M,i,j)) = n -' 1 by ; :: 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 ;
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 ;
hence width (Deleting (M,i,j)) = n -' 1 by A1, A8, Th3; :: thesis: verum
end;
end;