:: deftheorem defines exp*- INTEGR10:def 11 :
for s being Real
for b₂ being Function of REAL,REAL holds
( b₂ = exp*- s iff for t being Real holds b₂ . t = exp_R . (- (s * t)) );