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 A6: ( 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 ) ) ; :: 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 A7: ( 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 ) ) ; :: 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 AS1: s in dom f1 ; :: thesis: f1 . s = f2 . s
A8: f1 . s = infty_ext_right_integral (f (#) (exp*- s)),0 by A6, AS1;
thus f1 . s = f2 . s by A6, A7, A8, AS1; :: thesis: verum

end;

hence f1 = f2 by A6, A7, PARTFUN1:34; :: thesis: verum