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 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

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 :: thesis: for x being Element of X st x in dom g holds

g . x = h . x

hence
g = h
by A4, A6, PARTFUN1:5; :: thesis: verumg . x = h . x

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 = lim (f # x) by A5;

hence g . x = h . x by A4, A6, A7, A8; :: thesis: verum

end;assume A8: x in dom g ; :: thesis: g . x = h . x

then g . x = lim (f # x) by A5;

hence g . x = h . x by A4, A6, A7, A8; :: thesis: verum