let D be non empty set ; :: thesis: for i being Nat
for A being Matrix of D
for P being finite without_zero Subset of NAT st i in Seg (card P) holds
Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))
let i be Nat; :: thesis: for A being Matrix of D
for P being finite without_zero Subset of NAT st i in Seg (card P) holds
Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))
let A be Matrix of D; :: thesis: for P being finite without_zero Subset of NAT st i in Seg (card P) holds
Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))
let P be finite without_zero Subset of NAT; :: thesis: ( i in Seg (card P) implies Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i)) )
assume A1: i in Seg (card P) ; :: thesis: Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))
set S = Seg (width A);
set sP = Sgm P;
len (Line (A,((Sgm P) . i))) = width A by MATRIX_0:def 7;
then A2: dom (Line (A,((Sgm P) . i))) = Seg (width A) by FINSEQ_1:def 3;
Sgm (Seg (width A)) = idseq (width A) by FINSEQ_3:48;
then (Line (A,((Sgm P) . i))) * (Sgm (Seg (width A))) = Line (A,((Sgm P) . i)) by A2, RELAT_1:52;
hence Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i)) by A1, Th47; :: thesis: verum