:: deftheorem defines @ HILB10_2:def 1 :
for n being Nat
for p being b₁ -element real-valued XFinSequence holds @ p = p;