defpred S₁[ Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)), set ] means for y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - $1 holds
$2 = Rn->S1 ((f . $1) - (f . y));
A1: for x being Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) ex z being Element of (Tunit_circle n) st S₁[x,z]

proof

let x be Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)); :: thesis: ex z being Element of (Tunit_circle n) st S₁[x,z]
reconsider y = - x as Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) by TOPREALC:60;
reconsider z = Rn->S1 ((f . x) - (f . y)) as Point of (Tunit_circle n) ;
take z ; :: thesis: S₁[x,z]
thus S₁[x,z] ; :: thesis: verum

end;

ex g being Function of (Tcircle ((0. (TOP-REAL (n + 1))),1)),(Tunit_circle n) st
for x being Element of (Tcircle ((0. (TOP-REAL (n + 1))),1)) holds S₁[x,g . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of (Tunit_circle (n + 1)),(Tunit_circle n) st
for x, y being Point of (Tcircle ((0. (TOP-REAL (n + 1))),1)) st y = - x holds
b₁ . x = Rn->S1 ((f . x) - (f . y)) ; :: thesis: verum