theorem Th33: :: TREES_1:34

for p being FinSequence holds ProperPrefixes p, dom p are_equipotent