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 that
A1: dom f = right_closed_halfline 0 and
A2: 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 Intf = One-sided_Laplace_transform f;
set F = a (#) (One-sided_Laplace_transform f);
A3: dom (a (#) (One-sided_Laplace_transform f)) = dom (One-sided_Laplace_transform f) by VALUED_1:def 5
.= right_open_halfline 0 by Def12 ;
A4: 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)) ) )
A5: (a (#) f) (#) (exp*- s) = a (#) (f (#) (exp*- s)) by RFUNCT_1:12;
assume 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)) )
then A6: f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 by A2;
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 ( (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 A6, A5, Th9; :: thesis: verum
end;
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 A7: 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 A8: s in dom (One-sided_Laplace_transform f) by A3, Def12;
thus infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) by A4, A3, A7
.= a * ((One-sided_Laplace_transform f) . s) by A8, 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 A4, A3, Def12; :: thesis: verum