let f, g be Function of (Tunit_circle n),(Tcircle (p,r)); :: 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 ) & ( for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
g . a = (r * b) + p ) implies f = g )
assume that
A5: 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 and
A6: for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
g . a = (r * b) + p ; :: thesis: f = g
let x be Point of (Tunit_circle n); :: according to FUNCT_2:def 8 :: thesis: f . x = g . x
reconsider y = x as Point of (TOP-REAL n) by PRE_TOPC:25;
thus f . x = (r * y) + p by A5
.= g . x by A6 ; :: thesis: verum