for n being Nat
for f being FinSequence of REAL
for D being set st f is FinSequence of D holds
( f | n is FinSequence of D & f /^ n is FinSequence of D )