theorem Th72: :: ANPROJ_8:89

for D being non empty set
for pf being FinSequence of D holds Line (<*pf*>,1) = pf