defpred S₁[ set ] means $1 in right_open_halfline 0 ;
reconsider a = a as Real by XREAL_0:def 1;
deffunc H₁( Real) -> Element of REAL = log a,$1;
consider f being PartFunc of REAL ,REAL such that
A1: for d being Element of REAL holds
( d in dom f iff S₁[d] ) and
A2: for d being Element of REAL st d in dom f holds
f /. d = H₁(d) from PARTFUN2:sch 2();
take f ; :: thesis: ( dom f = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f . d = log a,d ) )
for x being set st x in right_open_halfline 0 holds
x in dom f by A1;
then A3: right_open_halfline 0 c= dom f by TARSKI:def 3;
for x being set st x in dom f holds
x in right_open_halfline 0 by A1;
then dom f c= right_open_halfline 0 by TARSKI:def 3;
hence A4: dom f = right_open_halfline 0 by A3, XBOOLE_0:def 10; :: thesis: for d being Element of right_open_halfline 0 holds f . d = log a,d
let d be Element of right_open_halfline 0 ; :: thesis: f . d = log a,d
f /. d = log a,d by A2, A4;
hence f . d = log a,d by A4, PARTFUN1:def 8; :: thesis: verum