let a be Real; :: thesis: for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds
( f is onto & f is isometric )
consider A being real number such that
A1: A = ((2 * PI ) * (- [\(a / (2 * PI ))/])) + a and
A2: 0 <= A and
A3: A < 2 * PI by COMPLEX2:2;
reconsider A = A as Real by XREAL_0:def 1;
let f be Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)); :: thesis: ( f = Rotate a implies ( f is onto & f is isometric ) )
assume A4: f = Rotate a ; :: thesis: ( f is onto & f is isometric )
reconsider g = f as Function of (Euclid 2),(Euclid 2) ;
A5: Rotate A = Rotate a by A1, Lm3;
( g is onto & g is isometric )

proof

thus rng g = the carrier of (Euclid 2) :: according to FUNCT_2:def 3 :: thesis: g is isometric

proof

thus rng g c= the carrier of (Euclid 2) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (Euclid 2) c= rng g
let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in the carrier of (Euclid 2) or o in rng g )
assume o in the carrier of (Euclid 2) ; :: thesis: o in rng g
then reconsider p = o as Point of (TOP-REAL 2) by EUCLID:71;
set pz = (p `1 ) + ((p `2 ) * <i> );
reconsider pz = (p `1 ) + ((p `2 ) * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
set arg = Arg pz;

per cases ( pz <> 0 or pz = 0 ) ;

suppose A6: pz <> 0 ; :: thesis: o in rng g

per cases ( A <= Arg pz or A > Arg pz ) ;

suppose A <= Arg pz ; :: thesis: o in rng g

then A7: 0 <= (Arg pz) - A by XREAL_1:50;
set qz = Rotate pz,(- A);
A8: |.(Rotate pz,(- A)).| = |.pz.| by COMPLEX2:67;
( (Arg pz) - A <= Arg pz & Arg pz < 2 * PI ) by A2, COMPTRIG:52, XREAL_1:45;
then A9: (- A) + (Arg pz) < 2 * PI by XXREAL_0:2;
Rotate pz,(- A) <> 0 by A6, COMPLEX2:66;
then Arg (Rotate pz,(- A)) = (- A) + (Arg pz) by A7, A9, A8, COMPTRIG:def 1;
then A10: Rotate (Rotate pz,(- A)),A = pz by A8, COMPLEX2:19;
set q = |[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]|;
A11: dom g = the carrier of (Euclid 2) by FUNCT_2:def 1;
g . |[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| = |[(Re (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by A4, A5, Def3
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate (Rotate pz,(- A)),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]| by COMPLEX1:29
.= |[(Re pz),(Im pz)]| by A10, COMPLEX1:29
.= |[(p `1 ),(Im pz)]| by COMPLEX1:28
.= |[(p `1 ),(p `2 )]| by COMPLEX1:28
.= p by EUCLID:57 ;
hence o in rng g by A11, Lm1, FUNCT_1:def 5; :: thesis: verum

end;

suppose A > Arg pz ; :: thesis: o in rng g

then (Arg pz) - A < 0 by XREAL_1:51;
then A12: (2 * PI ) + ((Arg pz) - A) < 2 * PI by XREAL_1:32;
set qz = Rotate pz,(- A);
set q = |[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]|;
A13: dom g = the carrier of (Euclid 2) by FUNCT_2:def 1;
A14: |.(Rotate pz,(- A)).| = |.pz.| by COMPLEX2:67;
then Rotate pz,(- A) = (|.(Rotate pz,(- A)).| * (cos (((2 * PI ) * 1) + ((- A) + (Arg pz))))) + ((|.(Rotate pz,(- A)).| * (sin ((- A) + (Arg pz)))) * <i> ) by COMPLEX2:10;
then A15: Rotate pz,(- A) = (|.(Rotate pz,(- A)).| * (cos ((2 * PI ) + ((Arg pz) - A)))) + ((|.(Rotate pz,(- A)).| * (sin (((2 * PI ) * 1) + ((- A) + (Arg pz))))) * <i> ) by COMPLEX2:9;
( 0 <= (2 * PI ) - A & Arg pz >= 0 ) by A3, COMPTRIG:52, XREAL_1:50;
then A16: 0 <= ((2 * PI ) - A) + (Arg pz) ;
Rotate pz,(- A) <> 0 by A6, COMPLEX2:66;
then Arg (Rotate pz,(- A)) = (2 * PI ) + ((Arg pz) - A) by A16, A12, A15, COMPTRIG:def 1;
then Rotate (Rotate pz,(- A)),A = (|.(Rotate pz,(- A)).| * (cos (Arg pz))) + ((|.(Rotate pz,(- A)).| * (sin (((2 * PI ) * 1) + (Arg pz)))) * <i> ) by COMPLEX2:10;
then Rotate (Rotate pz,(- A)),A = (|.(Rotate pz,(- A)).| * (cos (Arg pz))) + ((|.(Rotate pz,(- A)).| * (sin (Arg pz))) * <i> ) by COMPLEX2:9;
then A17: Rotate (Rotate pz,(- A)),A = pz by A14, COMPLEX2:19;
g . |[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| = |[(Re (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by A4, A5, Def3
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `1 ) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((|[(Re (Rotate pz,(- A))),(Im (Rotate pz,(- A)))]| `2 ) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]| by EUCLID:56
.= |[(Re (Rotate (Rotate pz,(- A)),A)),(Im (Rotate ((Re (Rotate pz,(- A))) + ((Im (Rotate pz,(- A))) * <i> )),A))]| by COMPLEX1:29
.= |[(Re pz),(Im pz)]| by A17, COMPLEX1:29
.= |[(p `1 ),(Im pz)]| by COMPLEX1:28
.= |[(p `1 ),(p `2 )]| by COMPLEX1:28
.= p by EUCLID:57 ;
hence o in rng g by A13, Lm1, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

suppose A18: pz = 0 ; :: thesis: o in rng g

reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def 2;
set q = |[0 ,0 ]|;
A19: dom g = the carrier of (Euclid 2) by FUNCT_2:def 1;
A20: p `1 = 0 by A18, COMPLEX1:12, COMPLEX1:28;
g . |[0 ,0 ]| = |[(Re (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]| by A4, Def3
.= |[(Re (Rotate (z + ((|[0 ,0 ]| `2 ) * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]| by EUCLID:56
.= |[(Re (Rotate (z + (z * <i> )),a)),(Im (Rotate ((|[0 ,0 ]| `1 ) + ((|[0 ,0 ]| `2 ) * <i> )),a))]| by EUCLID:56
.= |[(Re (Rotate (z + (z * <i> )),a)),(Im (Rotate (z + ((|[0 ,0 ]| `2 ) * <i> )),a))]| by EUCLID:56
.= |[(Re (Rotate z,a)),(Im (Rotate z,a))]| by EUCLID:56
.= |[(Re z),(Im (Rotate z,a))]| by COMPLEX2:66
.= |[(Re z),(Im z)]| by COMPLEX2:66
.= p by A18, A20, COMPLEX1:12, EUCLID:57 ;
hence o in rng g by A19, Lm1, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

let X, Y be Point of (Euclid 2); :: according to VECTMETR:def 3 :: thesis: dist X,Y = dist (g . X),(g . Y)
reconsider x = X, y = Y, gx = g . X, gy = g . Y as Point of (TOP-REAL 2) by EUCLID:71;
A21: ( |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]| `1 = Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a) & |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]| `2 = Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a) ) by EUCLID:56;
reconsider xx = (x `1 ) + ((x `2 ) * <i> ), yy = (y `1 ) + ((y `2 ) * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
A22: ( |[(Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a)),(Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a))]| `1 = Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a) & |[(Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a)),(Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a))]| `2 = Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a) ) by EUCLID:56;
A23: ( Re ((y `1 ) + ((y `2 ) * <i> )) = y `1 & Im ((y `1 ) + ((y `2 ) * <i> )) = y `2 ) by COMPLEX1:28;
A24: ((sin a) ^2 ) + ((cos a) ^2 ) = 1 by SIN_COS:32;
A25: ( Re ((x `1 ) + ((x `2 ) * <i> )) = x `1 & Im ((x `1 ) + ((x `2 ) * <i> )) = x `2 ) by COMPLEX1:28;
( x = |[(x `1 ),(x `2 )]| & y = |[(y `1 ),(y `2 )]| ) by EUCLID:57;
hence dist X,Y = sqrt ((((x `1 ) - (y `1 )) ^2 ) + (((x `2 ) - (y `2 )) ^2 )) by GOBOARD6:9
.= sqrt ((((((x `1 ) * (x `1 )) - ((2 * (x `1 )) * (y `1 ))) + ((y `1 ) * (y `1 ))) * (((sin a) * (sin a)) + ((cos a) * (cos a)))) + (((((x `2 ) * (x `2 )) - ((2 * (x `2 )) * (y `2 ))) + ((y `2 ) * (y `2 ))) * (((sin a) ^2 ) + ((cos a) ^2 )))) by A24
.= sqrt ((((((x `1 ) * (cos a)) - ((x `2 ) * (sin a))) - (((y `1 ) * (cos a)) - ((y `2 ) * (sin a)))) ^2 ) + ((((((x `1 ) * (sin a)) + ((x `2 ) * (cos a))) ^2 ) - ((2 * (((x `1 ) * (sin a)) + ((x `2 ) * (cos a)))) * (((y `1 ) * (sin a)) + ((y `2 ) * (cos a))))) + ((((y `1 ) * (sin a)) + ((y `2 ) * (cos a))) ^2 )))
.= sqrt ((((Re (Rotate xx,a)) - (((y `1 ) * (cos a)) - ((y `2 ) * (sin a)))) ^2 ) + (((((x `1 ) * (sin a)) + ((x `2 ) * (cos a))) - (((y `1 ) * (sin a)) + ((y `2 ) * (cos a)))) ^2 )) by A25, COMPLEX2:70
.= sqrt ((((Re (Rotate xx,a)) - (((y `1 ) * (cos a)) - ((y `2 ) * (sin a)))) ^2 ) + (((Im (Rotate xx,a)) - (((y `1 ) * (sin a)) + ((y `2 ) * (cos a)))) ^2 )) by A25, COMPLEX2:70
.= sqrt ((((Re (Rotate xx,a)) - (Re (Rotate yy,a))) ^2 ) + (((Im (Rotate xx,a)) - (((y `1 ) * (sin a)) + ((y `2 ) * (cos a)))) ^2 )) by A23, COMPLEX2:70
.= sqrt ((((Re (Rotate xx,a)) - (Re (Rotate yy,a))) ^2 ) + (((Im (Rotate xx,a)) - (Im (Rotate yy,a))) ^2 )) by A23, COMPLEX2:70
.= dist |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]|,|[(Re (Rotate ((y `1 ) + ((y `2 ) * <i> )),a)),(Im (Rotate ((y `1 ) + ((y `2 ) * <i> )),a))]| by A21, A22, TOPREAL6:101
.= dist |[(Re (Rotate ((x `1 ) + ((x `2 ) * <i> )),a)),(Im (Rotate ((x `1 ) + ((x `2 ) * <i> )),a))]|,gy by A4, Def3
.= dist gx,gy by A4, Def3
.= dist (g . X),(g . Y) by TOPREAL6:def 1 ;
:: thesis: verum

end;

hence ( f is onto & f is isometric ) by Def2; :: thesis: verum