let f, g be Function of (Tcircle o,r),(Tcircle o,r); :: thesis: ( ( 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 ) ; :: thesis: f = g

now

let x be set ; :: thesis: ( x in the carrier of (Tcircle o,r) implies f . x = g . x )
assume A10: x in the carrier of (Tcircle o,r) ; :: thesis: f . x = g . x
A11: 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; :: thesis: verum

end;

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