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 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 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 (#) ()),0) ) )

for s being Real st s in dom g holds
g . s = infty_ext_right_integral ((f (#) ()),0)
proof
let s be Real; :: thesis: ( s in dom g implies g . s = infty_ext_right_integral ((f (#) ()),0) )
assume A6: s in dom g ; :: thesis: g . s = infty_ext_right_integral ((f (#) ()),0)
then g /. s = infty_ext_right_integral ((f (#) ()),0) by A4;
hence g . s = infty_ext_right_integral ((f (#) ()),0) by ; :: 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 (#) ()),0) ) ) by A5; :: thesis: verum