theorem Th33: :: TREES_1:34
for p being FinSequence holds ProperPrefixes p, dom p are_equipotent