defpred S_{1}[ set ] means $1 in dom (f . 0);

deffunc H_{1}( Element of X) -> Element of COMPLEX = In ((lim (f # $1)),COMPLEX);

consider g being PartFunc of X,COMPLEX such that

A1: ( ( for x being Element of X holds

( x in dom g iff S_{1}[x] ) ) & ( for x being Element of X st x in dom g holds

g /. x = H_{1}(x) ) )
from PARTFUN2:sch 2();

take g ; :: thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds

g . x = lim (f # x) ) )

( x in dom g iff x in dom (f . 0) ) by A1;

hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds

g . x = lim (f # x) ) ) by A2, TARSKI:2; :: thesis: verum

deffunc H

consider g being PartFunc of X,COMPLEX such that

A1: ( ( for x being Element of X holds

( x in dom g iff S

g /. x = H

take g ; :: thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds

g . x = lim (f # x) ) )

A2: now :: thesis: for x being Element of X st x in dom g holds

g . x = lim (f # x)

for x being object holds g . x = lim (f # x)

let x be Element of X; :: thesis: ( x in dom g implies g . x = lim (f # x) )

assume A3: x in dom g ; :: thesis: g . x = lim (f # x)

then g /. x = H_{1}(x)
by A1;

hence g . x = lim (f # x) by A3, PARTFUN1:def 6; :: thesis: verum

end;assume A3: x in dom g ; :: thesis: g . x = lim (f # x)

then g /. x = H

hence g . x = lim (f # x) by A3, PARTFUN1:def 6; :: thesis: verum

( x in dom g iff x in dom (f . 0) ) by A1;

hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds

g . x = lim (f # x) ) ) by A2, TARSKI:2; :: thesis: verum