defpred S₁[ real number , set ] means $2 = |[(cos (((2 * PI ) * r) * $1)),(sin (((2 * PI ) * r) * $1))]|;
A1: for x being Element of I[01] ex y being Element of the carrier of (Tunit_circle 2) st S₁[x,y]

proof

let x be Element of I[01] ; :: thesis: ex y being Element of the carrier of (Tunit_circle 2) st S₁[x,y]
set y = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]|;
|.(|[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| - |[0 ,0 ]|).| = |.|[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]|.| by EUCLID:58, RLVECT_1:26, RLVECT_1:27
.= sqrt (((|[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| `1 ) ^2 ) + ((|[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| `2 ) ^2 )) by JGRAPH_1:47
.= sqrt (((cos (((2 * PI ) * r) * x)) ^2 ) + ((|[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| `2 ) ^2 )) by EUCLID:56
.= sqrt (((cos (((2 * PI ) * r) * x)) ^2 ) + ((sin (((2 * PI ) * r) * x)) ^2 )) by EUCLID:56
.= 1 by SIN_COS:32, SQUARE_1:83 ;
then reconsider y = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| as Element of the carrier of (Tunit_circle 2) by Lm11, TOPREAL9:9;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

ex f being Function of the carrier of I[01] ,the carrier of (Tunit_circle 2) st
for x being Element of I[01] holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
hence ex b₁ being Function of I[01] ,(Tunit_circle 2) st
for x being Point of I[01] holds b₁ . x = |[(cos (((2 * PI ) * r) * x)),(sin (((2 * PI ) * r) * x))]| ; :: thesis: verum