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 that
A1: dom f = right_closed_halfline 0 and
A2: dom g = right_closed_halfline 0 and
A3: ( ( 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 Intg = One-sided_Laplace_transform g;
set Intf = One-sided_Laplace_transform f;
set F = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g);
A4: 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 ;
A5: 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 ) ) )
A6: (f + g) (#) (exp*- s) = (f (#) (exp*- s)) + (g (#) (exp*- s)) by RFUNCT_1:22;
A7: dom (g (#) (exp*- s)) = (dom g) /\ (dom (exp*- s)) by VALUED_1:def 4
.= (right_closed_halfline 0 ) /\ REAL by A2, FUNCT_2:def 1
.= right_closed_halfline 0 by XBOOLE_1:28 ;
assume 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 ) )
then A8: ( f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) by A3;
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 ;
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 A8, A6, A7, Th8; :: thesis: verum

end;

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 A9: 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 A10: s in dom (One-sided_Laplace_transform f) by A4, Def12;
A11: s in dom (One-sided_Laplace_transform g) by A4, A9, 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 A5, A4, A9
.= ((One-sided_Laplace_transform f) . s) + (infty_ext_right_integral (g (#) (exp*- s)),0 ) by A10, Def12
.= ((One-sided_Laplace_transform f) . s) + ((One-sided_Laplace_transform g) . s) by A11, Def12
.= ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s by A9, 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 A5, A4, Def12; :: thesis: verum