:: deftheorem Def2 defines pricefunction FINANCE1:def 2 :
for b₁ being Real_Sequence holds
( b₁ is pricefunction iff ( b₁ . 0 = 1 & ( for n being Element of NAT holds b₁ . n >= 0 ) ) );