for p being FinSequence holds
( p /^ 0 = p & ( for i being Nat st i >= len p holds
p /^ i = {} ) )