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 by MATRIX_1:def 3;

A2: 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 that
A3: 1 <= j and
A4: 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 A5: j in Seg (len M) by A3, A4;
then A6: j in dom M by FINSEQ_1:def 3;
Sgm (Seg (len M)) = idseq (len M) by FINSEQ_3:54;
then A7: (Sgm (Seg (len M))) . j = j by A5, FINSEQ_2:57;
len (Line M,j) = width M by MATRIX_1:def 8;
then A8: dom (Line M,j) = Seg (width M) by FINSEQ_1:def 3;
A9: card (Seg (len M)) = len M by FINSEQ_1:78;
then A10: Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),j = (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j by A5, MATRIX_2:10;
Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),j = (Line M,((Sgm (Seg (len M))) . j)) * (Sgm ((Seg (width M)) \ {i})) by A9, A5, Th47, XBOOLE_1:36;
then (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j = Del (Line M,j),i by A7, A10, A8, FINSEQ_3:def 2;
hence (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) . j = (DelCol M,i) . j by A6, MATRIX_2:def 6; :: thesis: verum

end;

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