theorem Th48: :: MATRIX13:48

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