:: deftheorem defines PO BHSP_5:def 3 :
for X being RealUnitarySpace
for x being Point of X
for p being FinSequence
for i being Nat holds PO (i,p,x) = the scalar of X . [x,(p . i)];