let j be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum

for A being Matrix of K st j in Seg (width A) holds

width (DelCol (A,j)) = (width A) -' 1

let K be Field; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum