for n being Nat
for x being Element of REAL n
for f being FinSequence st x <> 0* n & x = f holds
ex i being Element of NAT st
( 1 <= i & i <= n & f . i <> 0 )