for x being real-valued FinSequence
for i being Nat st x is positive & 1 <= i & i <= len x holds
( x | i is positive & x | i <> {} )