for D being non empty set
for pf being FinSequence of D st len pf = 3 holds
( Line ((<*pf*> @),1) = <*(pf . 1)*> & Line ((<*pf*> @),2) = <*(pf . 2)*> & Line ((<*pf*> @),3) = <*(pf . 3)*> )