theorem :: TREES_1:35

for p being FinSequence holds card (ProperPrefixes p) = len p