let f be PartFunc of REAL ,REAL ; :: thesis: 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) )
let a be Real; :: thesis: ( 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 ) implies ( ( 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) ) )
assume A1: ( 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 ) ) ; :: thesis: ( ( 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) )
set F = a (#) (One-sided_Laplace_transform f);
set Intf = One-sided_Laplace_transform f;
A3: for s being Real st s in right_open_halfline 0 holds
( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0 = a * (infty_ext_right_integral (f (#) (exp*- s)),0 ) )

proof

let s be Real; :: thesis: ( s in right_open_halfline 0 implies ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0 = a * (infty_ext_right_integral (f (#) (exp*- s)),0 ) ) )
assume A4: s in right_open_halfline 0 ; :: thesis: ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0 = a * (infty_ext_right_integral (f (#) (exp*- s)),0 ) )
A5: f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 by A4, A1;
A6: (a (#) f) (#) (exp*- s) = a (#) (f (#) (exp*- s)) by RFUNCT_1:24;
A7: dom (f (#) (exp*- s)) = (dom f) /\ (dom (exp*- s)) by VALUED_1:def 4
.= (right_closed_halfline 0 ) /\ REAL by A1, FUNCT_2:def 1
.= right_closed_halfline 0 by XBOOLE_1:28 ;
thus ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0 = a * (infty_ext_right_integral (f (#) (exp*- s)),0 ) ) by A5, A6, A7, Th10; :: thesis: verum

end;

A9: dom (a (#) (One-sided_Laplace_transform f)) = dom (One-sided_Laplace_transform f) by VALUED_1:def 5
.= right_open_halfline 0 by Def12 ;
for s being Real st s in dom (a (#) (One-sided_Laplace_transform f)) holds
(a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0

proof

let s be Real; :: thesis: ( s in dom (a (#) (One-sided_Laplace_transform f)) implies (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0 )
assume A10: s in dom (a (#) (One-sided_Laplace_transform f)) ; :: thesis: (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0
then A11: s in dom (One-sided_Laplace_transform f) by A9, Def12;
thus infty_ext_right_integral ((a (#) f) (#) (exp*- s)),0 = a * (infty_ext_right_integral (f (#) (exp*- s)),0 ) by A3, A9, A10
.= a * ((One-sided_Laplace_transform f) . s) by A11, Def12
.= (a (#) (One-sided_Laplace_transform f)) . s by VALUED_1:6 ; :: thesis: verum

end;

hence ( ( 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) ) by A3, A9, Def12; :: thesis: verum