defpred S_{1}[ set ] means $1 in right_open_halfline 0;

reconsider a = a as Real ;

deffunc H_{1}( Real) -> Element of REAL = In ((log (a,$1)),REAL);

consider f being PartFunc of REAL,REAL such that

A1: for d being Element of REAL holds

( d in dom f iff S_{1}[d] )
and

A2: for d being Element of REAL st d in dom f holds

f /. d = H_{1}(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 object 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 object 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 = H_{1}(d)
by A2, A4;

hence f . d = log (a,d) by A4, PARTFUN1:def 6; :: thesis: verum

reconsider a = a as Real ;

deffunc H

consider f being PartFunc of REAL,REAL such that

A1: for d being Element of REAL holds

( d in dom f iff S

A2: for d being Element of REAL st d in dom f holds

f /. d = H

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 object 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 object 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 = H

hence f . d = log (a,d) by A4, PARTFUN1:def 6; :: thesis: verum