(1 / 2) - 1 < 0 ;
then [\(1 / 2)/] = 0 by INT_1:def 6;
then A9: (1 / 2) - [\(1 / 2)/] = 1 / 2 ;
frac ((1 / 2) + i) = frac (1 / 2) by INT_1:66
.= 1 / 2 by A9, INT_1:def 8 ;
then A10: CircleMap . (R^1 ((1 / 2) + i)) = CircleMap . (R^1 ((1 / 2) + 0)) by Lm19, Th34;
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:8;
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:62;
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:8;
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:2;
A14: CircleMap (R^1 ((1 / 2) + i)) = (CircleMap (R^1 (1 / 2))) * f by Th41;
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;
then f is open by A16, A15, A17, TOPREALA:10;
hence CircleMap (R^1 ((1 / 2) + i)) is open by A14, A10, Lm64, TOPREALA:11; :: thesis: verum