let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( dom f1 = right_open_halfline 0 & ( for s being Real st s in dom f1 holds
f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) & dom f2 = right_open_halfline 0 & ( for s being Real st s in dom f2 holds
f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) implies f1 = f2 )
assume that
A7: dom f1 = right_open_halfline 0 and
A8: for s being Real st s in dom f1 holds
f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ; :: thesis: ( not dom f2 = right_open_halfline 0 or ex s being Real st
( s in dom f2 & not f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) or f1 = f2 )
assume that
A9: dom f2 = right_open_halfline 0 and
A10: for s being Real st s in dom f2 holds
f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ; :: thesis: f1 = f2
for s being Element of REAL st s in dom f1 holds
f1 . s = f2 . s

proof

let s be Element of REAL ; :: thesis: ( s in dom f1 implies f1 . s = f2 . s )
assume A11: s in dom f1 ; :: thesis: f1 . s = f2 . s
f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A8, A11;
hence f1 . s = f2 . s by A7, A9, A10, A11; :: thesis: verum

end;

hence f1 = f2 by A7, A9, PARTFUN1:5; :: thesis: verum