let f, g be PartFunc of REAL,REAL; ( 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 ) )
; ( ( 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;
( 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:10;
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
;
( (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;
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;
( 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))
;
((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
;
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; verum