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

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