let j, n be Nat; 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; 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; for i being Nat st j in Seg (width M) holds
width (Deleting (M,i,j)) = n -' 1
let i be Nat; ( j in Seg (width M) implies width (Deleting (M,i,j)) = n -' 1 )
assume A1:
j in Seg (width M)
; 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 )
;
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;
verum end; end;