let D be non empty set ; :: thesis: for i being Nat
for A being Matrix of D holds Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i
let i be Nat; :: thesis: for A being Matrix of D holds Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i
let A be Matrix of D; :: thesis: Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i
set SLA = Seg (len A);
set Si = (Seg (len A)) \ {i};
set S = Segm A,((Seg (len A)) \ {i}),(Seg (width A));
A1: dom A = Seg (len A) by FINSEQ_1:def 3;

per cases ( not i in dom A or i in dom A ) ;

suppose A2: not i in dom A ; :: thesis: Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i

then A3: Del A,i = A by FINSEQ_3:113;
(Seg (len A)) \ {i} = Seg (len A) by A1, A2, ZFMISC_1:65;
hence Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i by A3, Th46; :: thesis: verum

end;

suppose A4: i in dom A ; :: thesis: Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i

then consider m being Nat such that
A5: len A = m + 1 and
A6: len (Del A,i) = m by FINSEQ_3:113;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
card (Seg (len A)) = m + 1 by A5, FINSEQ_1:78;
then A7: card ((Seg (len A)) \ {i}) = m by A1, A4, STIRL2_1:65;

A8: now

reconsider A9 = A as Matrix of m + 1, width A,D by A5, MATRIX_1:20;
let j be Nat; :: thesis: ( 1 <= j & j <= m implies (Del A,i) . j = (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) . j )
assume that
A9: 1 <= j and
A10: j <= m ; :: thesis: (Del A,i) . j = (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) . j
j in NAT by ORDINAL1:def 13;
then A11: j in Seg m by A9, A10;
A12: dom A = Seg (len A) by FINSEQ_1:def 3;
A13: Del A,i = A * (Sgm ((Seg (len A)) \ {i})) by A1, FINSEQ_3:def 2;
A14: dom (Del A,i) = Seg m by A6, FINSEQ_1:def 3;
then A15: (Sgm ((Seg (len A)) \ {i})) . j in dom A by A11, A13, FUNCT_1:21;
(Del A,i) . j = A9 . ((Sgm ((Seg (len A)) \ {i})) . j) by A14, A11, A13, FUNCT_1:22;
hence (Del A,i) . j = Line A9,((Sgm ((Seg (len A)) \ {i})) . j) by A5, A15, A12, MATRIX_2:10
.= Line (Segm A,((Seg (len A)) \ {i}),(Seg (width A))),j by A7, A11, Th48
.= (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) . j by A7, A11, MATRIX_2:10 ;
:: thesis: verum

end;

len (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) = m by A7, MATRIX_1:def 3;
hence Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i by A6, A8, FINSEQ_1:18; :: thesis: verum

end;

end;