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) )
assume A1: ( i in Seg (card P) & Q c= Seg (width A) ) ; :: thesis: Line (Segm A,P,Q),i = (Line A,((Sgm P) . i)) * (Sgm Q)
then rng (Sgm Q) = Q by FINSEQ_1:def 13;
hence Line (Segm A,P,Q),i = (Line A,((Sgm P) . i)) * (Sgm Q) by A1, Th24; :: thesis: verum