:: deftheorem Def12 defines One-sided_Laplace_transform INTEGR10:def 12 :
for f, b₂ being PartFunc of REAL,REAL holds
( b₂ = One-sided_Laplace_transform f iff ( dom b₂ = right_open_halfline 0 & ( for s being Real st s in dom b₂ holds
b₂ . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) );