defpred S₁[ set ] means $1 in dom (f . 0);
deffunc H₁( 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₁[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H₁(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) ) )

A2: now :: thesis: for x being Element of X st x in dom g 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₁(x) by A1;
hence g . x = lim (f # x) by A3, PARTFUN1:def 6; :: thesis: verum

end;

for x being object holds
( 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