defpred S1[ 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 () st S1[x,y]
proof
let x be Element of R^1; :: thesis: ex y being Element of the carrier of () st S1[x,y]
set y = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|;
|.(|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| - ).| = |.|[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]|.| by
.= 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 ;
then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| is Element of the carrier of () by ;
hence ex y being Element of the carrier of () st S1[x,y] ; :: thesis: verum
end;
consider f being Function of the carrier of R^1, the carrier of () such that
A2: for x being Element of R^1 holds S1[x,f . x] from 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 ;
hence f . x = |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| by A2; :: thesis: verum