for f being PartFunc of REAL,REAL
for a being Real st dom f = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds
f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) holds
( ( for s being Real st s in right_open_halfline 0 holds
(a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) )