let f, g be Function of (Tcircle (o,r)),(Tcircle (o,r)); ( ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (y,p,o,r) ) ) & ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & g . x = HC (y,p,o,r) ) ) implies f = g )
assume that
A8:
for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & f . x = HC (y,p,o,r) )
and
A9:
for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & g . x = HC (y,p,o,r) )
; f = g
now for x being object st x in the carrier of (Tcircle (o,r)) holds
f . x = g . xlet x be
object ;
( x in the carrier of (Tcircle (o,r)) implies f . x = g . x )assume A10:
x in the
carrier of
(Tcircle (o,r))
;
f . x = g . xA11:
ex
y being
Point of
(TOP-REAL n) st
(
x = y &
f . x = HC (
y,
p,
o,
r) )
by A8, A10;
ex
y being
Point of
(TOP-REAL n) st
(
x = y &
g . x = HC (
y,
p,
o,
r) )
by A9, A10;
hence
f . x = g . x
by A11;
verum end;
hence
f = g
by FUNCT_2:12; verum