let F, G be Function of (Tunit_circle (n + 1)),(Tunit_circle n); :: thesis: ( ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
F . x = Rn->S1 ((f . x) - (f . y)) ) & ( for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
G . x = Rn->S1 ((f . x) - (f . y)) ) implies F = G )
assume that
A2: for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
F . x = Rn->S1 ((f . x) - (f . y)) and
A3: for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
G . x = Rn->S1 ((f . x) - (f . y)) ; :: thesis: F = G
let p be Point of (Tunit_circle (n + 1)); :: according to FUNCT_2:def 8 :: thesis: F . p = G . p
reconsider p2 = p as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ;
reconsider p1 = - p as Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
thus F . p = Rn->S1 ((f . p2) - (f . p1)) by A2
.= G . p by A3 ; :: thesis: verum