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:29;
A2: the carrier of (R^1 | (R^1 ].i,(i + 1).[)) = R^1 ].i,(i + 1).[ by PRE_TOPC:29;
dom (AffineMap 1,(- i)) = REAL by FUNCT_2:def 1;
then A3: dom ((AffineMap 1,(- i)) | ].(0 + i),((0 + i) + p1).[) = ].i,(i + 1).[ by RELAT_1:91;
A4: rng ((AffineMap 1,(- i)) | ].(0 + i),((0 + i) + p1).[) = ].0 ,(0 + 1).[ by Lm26;
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:4;
A5: CircleMap (R^1 (0 + i)) = (CircleMap (R^1 0 )) * f by Th42;
A6: CircleMap . (R^1 i) = c[10] by Th33
.= CircleMap . (R^1 0 ) by Th33 ;
A7: ( R^1 | (R^1 (dom (AffineMap 1,(- i)))) = R^1 & R^1 | (R^1 (rng (AffineMap 1,(- i)))) = R^1 ) by Lm13;
A8: R^1 (AffineMap 1,(- i)) = AffineMap 1,(- i) ;
f is onto by A1, A4, FUNCT_2:def 3;
then f is open by A7, A8, TOPREALA:31;
hence CircleMap (R^1 i) is open by A5, A6, Lm63, TOPREALA:32; :: thesis: verum