defpred S_{1}[ 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 S_{1}[d,c] ) ) & ( for d being Element of REAL st d in dom g holds

S_{1}[d,g /. d] ) )
from PARTFUN2:sch 1();

A2: for d being Real holds

( d in dom g iff ex c being Real st S_{1}[d,c] )

S_{1}[d,g /. d]
by A1;

A5: dom g = right_open_halfline 0

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)

g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) by A5; :: thesis: verum

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

S

A2: for d being Real holds

( d in dom g iff ex c being Real st S

proof

A4:
for d being Real st d in dom g holds
let d be Real; :: thesis: ( d in dom g iff ex c being Real st S_{1}[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 S_{1}[d,c] )
by A1; :: thesis: ( ex c being Real st S_{1}[d,c] implies d in dom g )

given c being Real such that A3: S_{1}[d,c]
; :: thesis: d in dom g

reconsider c = c as Element of REAL by XREAL_0:def 1;

S_{1}[dd,c]
by A3;

then dd in dom g by A1;

hence d in dom g ; :: thesis: verum

end;reconsider dd = d as Element of REAL by XREAL_0:def 1;

thus ( d in dom g implies ex c being Real st S

given c being Real such that A3: S

reconsider c = c as Element of REAL by XREAL_0:def 1;

S

then dd in dom g by A1;

hence d in dom g ; :: thesis: verum

S

A5: dom g = right_open_halfline 0

proof

take
g
; :: thesis: ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds
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 )

end;reconsider s = s1 as Real ;

( s in right_open_halfline 0 implies s in dom g )

proof

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
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;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

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

hence
( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds
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;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

g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) by A5; :: thesis: verum