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