defpred S₁[ Element of REAL , Element of REAL ] means ( $1 in right_open_halfline 0 & $2 = infty_ext_right_integral (f (#) (exp*- $1)),0 );
consider g being PartFunc of REAL ,REAL such that
A1: ( ( for d being Element of REAL holds
( d in dom g iff ex c being Element of REAL st S₁[d,c] ) ) & ( for d being Element of REAL st d in dom g holds
S₁[d,g /. d] ) ) from PARTFUN2:sch 1();
A2: dom g = right_open_halfline 0

proof

let s1 be real number ; :: according to MEMBERED:def 15 :: thesis: ( ( not s1 in dom g or s1 in right_open_halfline 0 ) & ( not s1 in right_open_halfline 0 or s1 in dom g ) )
reconsider s = s1 as Real by XREAL_0:def 1;
( s in right_open_halfline 0 implies s in dom g )

proof

assume s in right_open_halfline 0 ; :: thesis: s in dom g
then ex y being Element of REAL st
( s in right_open_halfline 0 & y = infty_ext_right_integral (f (#) (exp*- s)),0 ) ;
hence s in dom g by A1; :: thesis: verum

end;

hence ( ( not s1 in dom g or s1 in right_open_halfline 0 ) & ( not s1 in right_open_halfline 0 or s1 in dom g ) ) by A1; :: thesis: verum

end;

take g ; :: thesis: ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds
g . s = infty_ext_right_integral (f (#) (exp*- s)),0 ) )
for s being Real st s in dom g holds
g . s = infty_ext_right_integral (f (#) (exp*- s)),0

proof

let s be Real; :: thesis: ( s in dom g implies g . s = infty_ext_right_integral (f (#) (exp*- s)),0 )
assume A3: s in dom g ; :: thesis: g . s = infty_ext_right_integral (f (#) (exp*- s)),0
then g /. s = infty_ext_right_integral (f (#) (exp*- s)),0 by A1;
hence g . s = infty_ext_right_integral (f (#) (exp*- s)),0 by A3, PARTFUN1:def 8; :: thesis: verum

end;

hence ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds
g . s = infty_ext_right_integral (f (#) (exp*- s)),0 ) ) by A2; :: thesis: verum