theorem Th81: :: MSAFREE4:81

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