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

let a be Real; :: thesis: ( dom f = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds
f (#) () is_+infty_ext_Riemann_integrable_on 0 ) implies ( ( for s being Real st s in right_open_halfline 0 holds
(a (#) f) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) ) )

assume that
A1: dom f = right_closed_halfline 0 and
A2: for s being Real st s in right_open_halfline 0 holds
f (#) () is_+infty_ext_Riemann_integrable_on 0 ; :: thesis: ( ( for s being Real st s in right_open_halfline 0 holds
(a (#) f) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) )

set Intf = One-sided_Laplace_transform f;
set F = a (#) ;
A3: dom () = dom 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) (#) () is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) ()),0) = a * (infty_ext_right_integral ((f (#) ()),0)) )
proof end;
for s being Real st s in dom () holds
() . s = infty_ext_right_integral (((a (#) f) (#) ()),0)
proof
let s be Real; :: thesis: ( s in dom () implies () . s = infty_ext_right_integral (((a (#) f) (#) ()),0) )
assume A7: s in dom () ; :: thesis: () . s = infty_ext_right_integral (((a (#) f) (#) ()),0)
then A8: s in dom by ;
thus infty_ext_right_integral (((a (#) f) (#) ()),0) = a * (infty_ext_right_integral ((f (#) ()),0)) by A4, A3, A7
.= a * () by
.= () . s by VALUED_1:6 ; :: thesis: verum
end;
hence ( ( for s being Real st s in right_open_halfline 0 holds
(a (#) f) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) ) by ; :: thesis: verum