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

proof

let s be Real; :: thesis: ( s in right_open_halfline 0 implies ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((f + g) (#) (exp*- s)),0 = (infty_ext_right_integral (f (#) (exp*- s)),0 ) + (infty_ext_right_integral (g (#) (exp*- s)),0 ) ) )
assume A4: s in right_open_halfline 0 ; :: thesis: ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((f + g) (#) (exp*- s)),0 = (infty_ext_right_integral (f (#) (exp*- s)),0 ) + (infty_ext_right_integral (g (#) (exp*- s)),0 ) )
A5: f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 by A4, A1;
A6: g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 by A4, A1;
A7: (f + g) (#) (exp*- s) = (f (#) (exp*- s)) + (g (#) (exp*- s)) by RFUNCT_1:22;
A8: 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 ;
dom (g (#) (exp*- s)) = (dom g) /\ (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 ;
hence ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral ((f + g) (#) (exp*- s)),0 = (infty_ext_right_integral (f (#) (exp*- s)),0 ) + (infty_ext_right_integral (g (#) (exp*- s)),0 ) ) by A5, A6, A7, A8, Th9; :: thesis: verum

end;

A10: dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) = (dom (One-sided_Laplace_transform f)) /\ (dom (One-sided_Laplace_transform g)) by VALUED_1:def 1
.= (right_open_halfline 0 ) /\ (dom (One-sided_Laplace_transform g)) by Def12
.= (right_open_halfline 0 ) /\ (right_open_halfline 0 ) by Def12
.= right_open_halfline 0 ;
for s being Real st s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) holds
((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral ((f + g) (#) (exp*- s)),0

proof

let s be Real; :: thesis: ( s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) implies ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral ((f + g) (#) (exp*- s)),0 )
assume A11: s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) ; :: thesis: ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral ((f + g) (#) (exp*- s)),0
then A12: s in dom (One-sided_Laplace_transform f) by A10, Def12;
A13: s in dom (One-sided_Laplace_transform g) by A11, A10, Def12;
thus infty_ext_right_integral ((f + g) (#) (exp*- s)),0 = (infty_ext_right_integral (f (#) (exp*- s)),0 ) + (infty_ext_right_integral (g (#) (exp*- s)),0 ) by A3, A10, A11
.= ((One-sided_Laplace_transform f) . s) + (infty_ext_right_integral (g (#) (exp*- s)),0 ) by A12, Def12
.= ((One-sided_Laplace_transform f) . s) + ((One-sided_Laplace_transform g) . s) by A13, Def12
.= ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s by A11, VALUED_1:def 1 ; :: thesis: verum

end;

hence ( ( for s being Real st s in right_open_halfline 0 holds
(f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g) ) by A3, A10, Def12; :: thesis: verum