defpred S1[ set ] means $1 in right_open_halfline 0;
reconsider a = a as Real ;
deffunc H1( 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 S1[d] )
and
A2:
for d being Element of REAL st d in dom f holds
f /. d = H1(d)
from PARTFUN2:sch 2();
take
f
; ( 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; for d being Element of right_open_halfline 0 holds f . d = log (a,d)
let d be Element of right_open_halfline 0; f . d = log (a,d)
f /. d = H1(d)
by A2, A4;
hence
f . d = log (a,d)
by A4, PARTFUN1:def 6; verum