hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: INT c= CircleMap " {c[10]}

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in INT or i in CircleMap " {c[10]} )let i be object ; :: thesis: ( i in CircleMap " {c[10]} implies i in INT )

assume A1: i in CircleMap " {c[10]} ; :: thesis: i in INT

then reconsider x = i as Real ;

CircleMap . i in {c[10]} by A1, FUNCT_2:38;

then CircleMap . i = c[10] by TARSKI:def 1;

then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| = |[1,0]| by Def11;

then cos ((2 * PI) * x) = 1 by SPPOL_2:1;

hence i in INT by SIN_COS6:44; :: thesis: verum

end;assume A1: i in CircleMap " {c[10]} ; :: thesis: i in INT

then reconsider x = i as Real ;

CircleMap . i in {c[10]} by A1, FUNCT_2:38;

then CircleMap . i = c[10] by TARSKI:def 1;

then |[(cos ((2 * PI) * x)),(sin ((2 * PI) * x))]| = |[1,0]| by Def11;

then cos ((2 * PI) * x) = 1 by SPPOL_2:1;

hence i in INT by SIN_COS6:44; :: thesis: verum

assume i in INT ; :: thesis: i in CircleMap " {c[10]}

then reconsider i = i as Integer ;

CircleMap . i = c[10] by Th32;

then A2: CircleMap . i in {c[10]} by TARSKI:def 1;

i in the carrier of R^1 by TOPMETR:17, XREAL_0:def 1;

hence i in CircleMap " {c[10]} by A2, FUNCT_2:38; :: thesis: verum