theorem Th2: :: EUCLID_9:2

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