let j be Nat; for K being Field
for A being Matrix of K st j in Seg (width A) holds
width (DelCol (A,j)) = (width A) -' 1
let K be Field; for A being Matrix of K st j in Seg (width A) holds
width (DelCol (A,j)) = (width A) -' 1
let A be Matrix of K; ( j in Seg (width A) implies width (DelCol (A,j)) = (width A) -' 1 )
set DC = DelCol (A,j);
A1:
len (DelCol (A,j)) = len A
by MATRIX_0:def 13;
assume A2:
j in Seg (width A)
; width (DelCol (A,j)) = (width A) -' 1
then
Seg (width A) <> {}
;
then
width A <> 0
;
then
len A > 0
by MATRIX_0:def 3;
then consider t being FinSequence such that
A3:
t in rng (DelCol (A,j))
and
A4:
len t = width (DelCol (A,j))
by A1, MATRIX_0:def 3;
consider k9 being object such that
A5:
k9 in dom (DelCol (A,j))
and
A6:
(DelCol (A,j)) . k9 = t
by A3, FUNCT_1:def 3;
k9 in Seg (len (DelCol (A,j)))
by A5, FINSEQ_1:def 3;
then consider k being Nat such that
A7:
k9 = k
and
1 <= k
and
k <= len (DelCol (A,j))
;
k in dom A
by A1, A5, A7, FINSEQ_3:29;
then A8:
t = Del ((Line (A,k)),j)
by A6, A7, MATRIX_0:def 13;
A9:
len (Line (A,k)) = width A
by MATRIX_0:def 7;
then
dom (Line (A,k)) = Seg (width A)
by FINSEQ_1:def 3;
hence
width (DelCol (A,j)) = (width A) -' 1
by A2, A4, A9, A8, Th1; verum