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_1:def 8;
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:54;
then (Line A,((Sgm P) . i)) * (Sgm (Seg (width A))) = Line A,((Sgm P) . i) by A2, RELAT_1:78;
hence Line (Segm A,P,(Seg (width A))),i = Line A,((Sgm P) . i) by A1, Th47; :: thesis: verum