let f, g be Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)); :: thesis: ( ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (p,y,o,r) ) ) & ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & g . x = HC (p,y,o,r) ) ) implies f = g )
assume that
A7: for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (p,y,o,r) ) and
A8: for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & g . x = HC (p,y,o,r) ) ; :: thesis: f = g

now :: thesis: for x being object st x in the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) holds
f . x = g . x

let x be object ; :: thesis: ( x in the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) implies f . x = g . x )
assume A9: x in the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ; :: thesis: f . x = g . x
A10: ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (p,y,o,r) ) by A7, A9;
ex y being Point of (TOP-REAL n) st
( x = y & g . x = HC (p,y,o,r) ) by A8, A9;
hence f . x = g . x by A10; :: thesis: verum

end;

hence f = g by FUNCT_2:12; :: thesis: verum