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

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 )
;

end;

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;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