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 not i in dom A ; :: thesis: Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i

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

end;

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

then consider m being Nat such that
A3: ( len A = m + 1 & 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 A3, FINSEQ_1:78;
then A4: card ((Seg (len A)) \ {i}) = m by A1, A2, STIRL2_1:65;
then A5: len (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) = m by MATRIX_1:def 3;

now

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 A6: ( 1 <= j & j <= m ) ; :: thesis: (Del A,i) . j = (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) . j
reconsider A' = A as Matrix of m + 1, width A,D by A3, MATRIX_1:20;
j in NAT by ORDINAL1:def 13;
then A7: ( dom (Del A,i) = Seg m & j in Seg m & Del A,i = A * (Sgm ((Seg (len A)) \ {i})) ) by A1, A3, A6, FINSEQ_1:def 3, FINSEQ_3:def 2;
then ( (Del A,i) . j = A' . ((Sgm ((Seg (len A)) \ {i})) . j) & (Sgm ((Seg (len A)) \ {i})) . j in dom A & dom A = Seg (len A) ) by FINSEQ_1:def 3, FUNCT_1:21, FUNCT_1:22;
hence (Del A,i) . j = Line A',((Sgm ((Seg (len A)) \ {i})) . j) by A3, MATRIX_2:10
.= Line (Segm A,((Seg (len A)) \ {i}),(Seg (width A))),j by A4, A7, Th48
.= (Segm A,((Seg (len A)) \ {i}),(Seg (width A))) . j by A4, A7, MATRIX_2:10 ;
:: thesis: verum

end;

hence Segm A,((Seg (len A)) \ {i}),(Seg (width A)) = Del A,i by A3, A5, FINSEQ_1:18; :: thesis: verum

end;

end;