let g, h be PartFunc of X,ExtREAL; :: thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = lim (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = lim (f # x) ; :: thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = lim (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = lim (f # x) ; :: thesis: g = h

now

let x be Element of X; :: thesis: ( x in dom g implies g /. x = h /. x )
assume A8: x in dom g ; :: thesis: g /. x = h /. x
then g /. x = g . x by PARTFUN1:def 6;
then g /. x = lim (f # x) by A5, A8;
then g /. x = h . x by A4, A6, A7, A8;
hence g /. x = h /. x by A4, A6, A8, PARTFUN1:def 6; :: thesis: verum

end;

hence g = h by A4, A6, PARTFUN2:1; :: thesis: verum