defpred S_{1}[ Real, set ] means $2 = |[(cos ((2 * PI) * $1)),(sin ((2 * PI) * $1))]|;

A1: for x being Element of R^1 ex y being Element of the carrier of (Tunit_circle 2) st S_{1}[x,y]

A2: for x being Element of R^1 holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A1);

take f ; :: thesis: for x being Real holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|

let x be Real; :: thesis: f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|

x is Point of R^1 by TOPMETR:17, XREAL_0:def 1;

hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| by A2; :: thesis: verum

A1: for x being Element of R^1 ex y being Element of the carrier of (Tunit_circle 2) st S

proof

consider f being Function of the carrier of R^1, the carrier of (Tunit_circle 2) such that
let x be Element of R^1; :: thesis: ex y being Element of the carrier of (Tunit_circle 2) st S_{1}[x,y]

set y = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|;

|.(|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| - |[0,0]|).| = |.|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|.| by EUCLID:54, RLVECT_1:13

.= sqrt (((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `1) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `2) ^2)) by JGRAPH_1:30

.= sqrt (((cos ((2 * PI) * x)) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `2) ^2)) by EUCLID:52

.= sqrt (((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) by EUCLID:52

.= 1 by SIN_COS:29, SQUARE_1:18 ;

then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| is Element of the carrier of (Tunit_circle 2) by Lm13, TOPREAL9:9;

hence ex y being Element of the carrier of (Tunit_circle 2) st S_{1}[x,y]
; :: thesis: verum

end;set y = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|;

|.(|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| - |[0,0]|).| = |.|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|.| by EUCLID:54, RLVECT_1:13

.= sqrt (((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `1) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `2) ^2)) by JGRAPH_1:30

.= sqrt (((cos ((2 * PI) * x)) ^2) + ((|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| `2) ^2)) by EUCLID:52

.= sqrt (((cos ((2 * PI) * x)) ^2) + ((sin ((2 * PI) * x)) ^2)) by EUCLID:52

.= 1 by SIN_COS:29, SQUARE_1:18 ;

then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| is Element of the carrier of (Tunit_circle 2) by Lm13, TOPREAL9:9;

hence ex y being Element of the carrier of (Tunit_circle 2) st S

A2: for x being Element of R^1 holds S

take f ; :: thesis: for x being Real holds f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|

let x be Real; :: thesis: f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|

x is Point of R^1 by TOPMETR:17, XREAL_0:def 1;

hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| by A2; :: thesis: verum