defpred S1[ Real, 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 S1[d,c] ) ) & ( for d being Element of REAL st d in dom g holds
S1[d,g /. d] ) ) from PARTFUN2:sch 1();
 A2: for d being Real holds
( d in dom g iff ex c being Real st S1[d,c] )
proof
let d be Real; :: thesis: ( d in dom g iff ex c being Real st S1[d,c] )
reconsider dd = d as Element of REAL by XREAL_0:def 1;
thus ( d in dom g implies ex c being Real st S1[d,c] ) by A1; :: thesis: ( ex c being Real st S1[d,c] implies d in dom g )
given c being Real such that A3: S1[d,c] ; :: thesis: d in dom g
reconsider c = c as Element of REAL by XREAL_0:def 1;
S1[dd,c] by A3;
then dd in dom g by A1;
hence d in dom g ; :: thesis: verum
end;
A4: for d being Real st d in dom g holds
S1[d,g /. d] by A1;
A5: dom g = right_open_halfline 0
proof
let s1 be Real; :: 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 ;
( 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 Real st
( s in right_open_halfline 0 & y = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ;
hence s in dom g by A2; :: 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 A4; :: 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 A6: 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 A4;
hence g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A6, PARTFUN1:def 6; :: 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 A5; :: thesis: verum