set U = Tunit_circle n;
set C = Tcircle (p,r);
defpred S₁[ Point of (Tunit_circle n), set ] means ex w being Point of (TOP-REAL n) st
( w = $1 & $2 = (r * w) + p );
A1: n in NAT by ORDINAL1:def 12;
then A2: the carrier of (Tcircle (p,r)) = Sphere (p,r) by TOPREALB:9;
A3: for u being Point of (Tunit_circle n) ex y being Point of (Tcircle (p,r)) st S₁[u,y]

proof

let u be Point of (Tunit_circle n); :: thesis: ex y being Point of (Tcircle (p,r)) st S₁[u,y]
reconsider v = u as Point of (TOP-REAL n) by PRE_TOPC:25;
set y = (r * v) + p;
|.(((r * v) + p) - p).| = |.(r * v).| by RLVECT_4:1
.= |.r.| * |.v.| by TOPRNS_1:7
.= r * |.v.| by ABSVALUE:def 1
.= r * 1 by A1, TOPREALB:12 ;
then reconsider y = (r * v) + p as Point of (Tcircle (p,r)) by A2, TOPREAL9:9;
take y ; :: thesis: S₁[u,y]
thus S₁[u,y] ; :: thesis: verum

end;

consider f being Function of (Tunit_circle n),(Tcircle (p,r)) such that
A4: for x being Point of (Tunit_circle n) holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
take f ; :: thesis: for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p
let a be Point of (Tunit_circle n); :: thesis: for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p
let b be Point of (TOP-REAL n); :: thesis: ( a = b implies f . a = (r * b) + p )
S₁[a,f . a] by A4;
hence ( a = b implies f . a = (r * b) + p ) ; :: thesis: verum