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:104;
(Seg (len A)) \ {i} = Seg (len A) by A1, A2, ZFMISC_1:57;
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:104;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
card (Seg (len A)) = m + 1 by A5, FINSEQ_1:57;
then A7: card ((Seg (len A)) \ {i}) = m by A1, A4, STIRL2_1:55;
A8: now :: thesis: for j being Nat st 1 <= j & j <= m holds
(Del (A,i)) . j = (Segm (A,((Seg (len A)) \ {i}),(Seg (width A)))) . j
reconsider A9 = A as Matrix of m + 1, width A,D by A5, MATRIX_0: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
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:11;
(Del (A,i)) . j = A9 . ((Sgm ((Seg (len A)) \ {i})) . j) by A14, A11, A13, FUNCT_1:12;
hence (Del (A,i)) . j = Line (A9,((Sgm ((Seg (len A)) \ {i})) . j)) by A5, A15, A12, MATRIX_0:52
.= 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_0:52 ;
:: thesis: verum
end;
len (Segm (A,((Seg (len A)) \ {i}),(Seg (width A)))) = m by A7, MATRIX_0:def 2;
hence Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i) by A6, A8; :: thesis: verum
end;
end;