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:57;
then A1: len (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) = len M by MATRIX_0:def 2;

A2: now :: thesis: for j being Nat st 1 <= j & j <= len M holds
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) . j = (DelCol (M,i)) . j

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
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:48;
then A7: (Sgm (Seg (len M))) . j = j by A5, FINSEQ_2:49;
len (Line (M,j)) = width M by MATRIX_0:def 7;
then A8: dom (Line (M,j)) = Seg (width M) by FINSEQ_1:def 3;
A9: card (Seg (len M)) = len M by FINSEQ_1:57;
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_0:52;
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_0:def 13; :: thesis: verum

end;

len (DelCol (M,i)) = len M by MATRIX_0:def 13;
hence Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i) by A1, A2; :: thesis: verum