let g, h be PartFunc of X,COMPLEX ; :: 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 A4: ( dom g = dom (f . 0 ) & ( 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 A5: ( dom h = dom (f . 0 ) & ( 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 A6: x in dom g ; :: thesis: g . x = h . x
then g . x = lim (f # x) by A4;
hence g . x = h . x by A4, A5, A6; :: thesis: verum

end;

hence g = h by A4, A5, PARTFUN1:34; :: thesis: verum