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: r is Real by XREAL_0:def 1;
A2: n in NAT by ORDINAL1:def 12;
then A3: the carrier of (Tcircle (p,r)) = Sphere (p,r) by TOPREALB:9;
A4: 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 EUCLID:48
.= (abs r) * |.v.| by A2, A1, TOPRNS_1:7
.= r * |.v.| by ABSVALUE:def 1
.= r * 1 by A2, TOPREALB:12 ;
then reconsider y = (r * v) + p as Point of (Tcircle (p,r)) by A2, A3, 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
A5: for x being Point of (Tunit_circle n) holds S₁[x,f . x] from FUNCT_2:sch 3(A4);
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 A5;
hence ( a = b implies f . a = (r * b) + p ) ; :: thesis: verum