let i be Nat; :: thesis: for K being Field
for M being Matrix of K holds Segm M,(Seg (len M)),((Seg (width M)) \ {i}) = DelCol M,i
let K be Field; :: thesis: for M being Matrix of K holds Segm M,(Seg (len M)),((Seg (width M)) \ {i}) = DelCol M,i
let M be Matrix of K; :: thesis: Segm M,(Seg (len M)),((Seg (width M)) \ {i}) = DelCol M,i
set SW = Seg (width M);
set Si = (Seg (width M)) \ {i};
set SL = Seg (len M);
set SEGM = Segm M,(Seg (len M)),((Seg (width M)) \ {i});
set D = DelCol M,i;
card (Seg (len M)) = len M by FINSEQ_1:78;
then A1: ( len (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = len M & len (DelCol M,i) = len M ) by MATRIX_1:def 3, MATRIX_2:def 6;

now

let j be Nat; :: thesis: ( 1 <= j & j <= len M implies (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j = (DelCol M,i) . j )
assume A2: ( 1 <= j & j <= len M ) ; :: thesis: (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j = (DelCol M,i) . j
j in NAT by ORDINAL1:def 13;
then ( card (Seg (len M)) = len M & j in Seg (len M) & (Seg (width M)) \ {i} c= Seg (width M) & Sgm (Seg (len M)) = idseq (len M) & len (Line M,j) = width M ) by A2, FINSEQ_1:78, FINSEQ_3:54, MATRIX_1:def 8, XBOOLE_1:36;
then ( Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),j = (Line M,((Sgm (Seg (len M))) . j)) * (Sgm ((Seg (width M)) \ {i})) & (Sgm (Seg (len M))) . j = j & Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),j = (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j & dom (Line M,j) = Seg (width M) & j in dom M ) by Th47, FINSEQ_1:def 3, FINSEQ_2:57, MATRIX_2:10;
then ( (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j = Del (Line M,j),i & (DelCol M,i) . j = Del (Line M,j),i ) by FINSEQ_3:def 2, MATRIX_2:def 6;
hence (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j = (DelCol M,i) . j ; :: thesis: verum

end;

hence Segm M,(Seg (len M)),((Seg (width M)) \ {i}) = DelCol M,i by A1, FINSEQ_1:18; :: thesis: verum