theorem Th47: :: MATRIX13:47

for D being non empty set
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)