defpred S1[ 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 S1[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 S1[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: S1[x,z]
thus S1[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 S1[x,g . x] from FUNCT_2:sch 3(A1);
 hence ex b1 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
b1 . x = Rn->S1 ((f . x) - (f . y)) ; :: thesis: verum