:: deftheorem Def3 defines Conv2 FINANCE6:def 2 :
for t being Real
for n being Nat holds
( ( n = 0 implies Conv2 (n,t) = 1 ) & ( not n = 0 implies Conv2 (n,t) = Conv (n,t) ) );