set F = AffineMap (1,(- i));
set f = (AffineMap (1,(- i))) | ].(0 + i),((0 + i) + p1).[;
A1: the carrier of (R^1 | (R^1 ].0,1.[)) = R^1 ].0,1.[ by PRE_TOPC:8;
dom (AffineMap (1,(- i))) = REAL by FUNCT_2:def 1;
then A2: dom ((AffineMap (1,(- i))) | ].(0 + i),((0 + i) + p1).[) = ].i,(i + 1).[ by RELAT_1:62;
A3: rng ((AffineMap (1,(- i))) | ].(0 + i),((0 + i) + p1).[) = ].0,(0 + 1).[ by Lm24;
the carrier of (R^1 | (R^1 ].i,(i + 1).[)) = R^1 ].i,(i + 1).[ by PRE_TOPC:8;
then reconsider f = (AffineMap (1,(- i))) | ].(0 + i),((0 + i) + p1).[ as Function of (R^1 | (R^1 ].i,(i + p1).[)),(R^1 | (R^1 ].0,(0 + p1).[)) by A1, A2, A3, FUNCT_2:2;
A4: CircleMap (R^1 (0 + i)) = (CircleMap (R^1 0)) * f by Th41;
A5: R^1 | (R^1 (rng (AffineMap (1,(- i))))) = R^1 by Lm12;
A6: CircleMap . (R^1 i) = c[10] by Th32
.= CircleMap . (R^1 0) by Th32 ;
A7: R^1 | (R^1 (dom (AffineMap (1,(- i))))) = R^1 by Lm12;
A8: R^1 (AffineMap (1,(- i))) = AffineMap (1,(- i)) ;
f is onto by A1, A3;
then f is open by A7, A5, A8, TOPREALA:10;
hence CircleMap (R^1 i) is open by A4, A6, Lm63, TOPREALA:11; :: thesis: verum