theorem Th61: :: ANPROJ_8:75

for D being non empty set
for pf being FinSequence of D holds width <*pf*> = len pf