for n being Nat
for f being b₁ -element real-valued FinSequence holds f in REAL n