(1 / 2) - 1 < 0 ;
then [\(1 / 2)/] = 0 by INT_1:def 4;
then A9: (1 / 2) - [\(1 / 2)/] = 1 / 2 ;
frac ((1 / 2) + i) = frac (1 / 2) by TOPREALA:1
.= 1 / 2 by A9, INT_1:def 6 ;
then A10: CircleMap . (R^1 ((1 / 2) + i)) = CircleMap . (R^1 ((1 / 2) + 0 )) by Lm19, Th35;
set F = AffineMap 1,(- i);
set f = (AffineMap 1,(- i)) | ].((1 / 2) + i),(((1 / 2) + i) + p1).[;
A11: the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) = R^1 ].(1 / 2),(3 / 2).[ by PRE_TOPC:29;
dom (AffineMap 1,(- i)) = REAL by FUNCT_2:def 1;
then A12: dom ((AffineMap 1,(- i)) | ].((1 / 2) + i),(((1 / 2) + i) + p1).[) = ].((1 / 2) + i),(((1 / 2) + i) + 1).[ by RELAT_1:91;
A13: rng ((AffineMap 1,(- i)) | ].((1 / 2) + i),(((1 / 2) + i) + p1).[) = ].(1 / 2),((1 / 2) + 1).[ by Lm24;
the carrier of (R^1 | (R^1 ].((1 / 2) + i),(((1 / 2) + i) + 1).[)) = R^1 ].((1 / 2) + i),(((1 / 2) + i) + 1).[ by PRE_TOPC:29;
then reconsider f = (AffineMap 1,(- i)) | ].((1 / 2) + i),(((1 / 2) + i) + p1).[ as Function of (R^1 | (R^1 ].((1 / 2) + i),(((1 / 2) + i) + p1).[)),(R^1 | (R^1 ].(1 / 2),((1 / 2) + p1).[)) by A11, A12, A13, FUNCT_2:4;
A14: CircleMap (R^1 ((1 / 2) + i)) = (CircleMap (R^1 (1 / 2))) * f by Th42;
A15: R^1 | (R^1 (rng (AffineMap 1,(- i)))) = R^1 by Lm12;
A16: R^1 | (R^1 (dom (AffineMap 1,(- i)))) = R^1 by Lm12;
A17: R^1 (AffineMap 1,(- i)) = AffineMap 1,(- i) ;
f is onto by A11, A13, FUNCT_2:def 3;
then f is open by A16, A15, A17, TOPREALA:31;
hence CircleMap (R^1 ((1 / 2) + i)) is open by A14, A10, Lm64, TOPREALA:32; :: thesis: verum