deffunc H₁( Real) -> Element of REAL = In ((exp_R . (- (s * $1))),REAL);
consider g being Function of REAL,REAL such that
A1: for x being Element of REAL holds g . x = H₁(x) from FUNCT_2:sch 4();
take g ; :: thesis: for t being Real holds g . t = exp_R . (- (s * t))
let x be Real; :: thesis: g . x = exp_R . (- (s * x))
x in REAL by XREAL_0:def 1;
then g . x = H₁(x) by A1;
hence g . x = exp_R . (- (s * x)) ; :: thesis: verum