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 (#) () is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds
g (#) () is_+infty_ext_Riemann_integrable_on 0 ) implies ( ( for s being Real st s in right_open_halfline 0 holds
(f + g) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + 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 (#) () is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds
g (#) () is_+infty_ext_Riemann_integrable_on 0 ) ) ; :: thesis: ( ( for s being Real st s in right_open_halfline 0 holds
(f + g) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = + )

set Intg = One-sided_Laplace_transform g;
set Intf = One-sided_Laplace_transform f;
set F = + ;
A4: dom = /\ by VALUED_1:def 1
.= /\ by Def12
.= /\ by Def12
.= right_open_halfline 0 ;
A5: for s being Real st s in right_open_halfline 0 holds
( (f + g) (#) () is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) ()),0) = (infty_ext_right_integral ((f (#) ()),0)) + (infty_ext_right_integral ((g (#) ()),0)) )
proof end;
for s being Real st s in dom holds
. s = infty_ext_right_integral (((f + g) (#) ()),0)
proof
let s be Real; :: thesis: ( s in dom implies . s = infty_ext_right_integral (((f + g) (#) ()),0) )
assume A9: s in dom ; :: thesis: . s = infty_ext_right_integral (((f + g) (#) ()),0)
then A10: s in dom by ;
A11: s in dom by ;
thus infty_ext_right_integral (((f + g) (#) ()),0) = (infty_ext_right_integral ((f (#) ()),0)) + (infty_ext_right_integral ((g (#) ()),0)) by A5, A4, A9
.= () + (infty_ext_right_integral ((g (#) ()),0)) by
.= () + () by
.= . s by ; :: thesis: verum
end;
hence ( ( for s being Real st s in right_open_halfline 0 holds
(f + g) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = + ) by ; :: thesis: verum