let D be non empty set ; :: thesis: for i being Nat
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
let i be Nat; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
let A be Matrix of D; :: thesis: for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
let P, Q be finite without_zero Subset of NAT; :: thesis: ( i in Seg (card P) & Q c= Seg (width A) implies Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q) )
rng (Sgm Q) = Q by FINSEQ_1:def 14;
hence ( i in Seg (card P) & Q c= Seg (width A) implies Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q) ) by Th24; :: thesis: verum