set B = [.r,(r + 1).[;
set A = ].r,(r + 1).[;
set X = Topen_unit_circle (CircleMap . r);
set f = CircleMap | ].r,(r + 1).[;
set g = CircleMap | [.r,(r + 1).[;
A1: ].r,(r + 1).[ c= [.r,(r + 1).[ by XXREAL_1:45;
A2: dom (CircleMap | ].r,(r + 1).[) = ].r,(r + 1).[ by Lm18, RELAT_1:62;
A3: the carrier of (Topen_unit_circle (CircleMap . r)) = the carrier of (Tunit_circle 2) \ {(CircleMap . r)} by Def10;
A4: rng (CircleMap | ].r,(r + 1).[) c= the carrier of (Topen_unit_circle (CircleMap . r))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (CircleMap | ].r,(r + 1).[) or y in the carrier of (Topen_unit_circle (CircleMap . r)) )
assume A5: y in rng (CircleMap | ].r,(r + 1).[) ; :: thesis: y in the carrier of (Topen_unit_circle (CircleMap . r))

now :: thesis: not y = CircleMap . r

A6: dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[ by Lm18, RELAT_1:62;
assume A7: y = CircleMap . r ; :: thesis: contradiction
r + 0 < r + 1 by XREAL_1:8;
then A8: r in [.r,(r + 1).[ by XXREAL_1:3;
consider x being object such that
A9: x in dom (CircleMap | ].r,(r + 1).[) and
A10: (CircleMap | ].r,(r + 1).[) . x = y by A5, FUNCT_1:def 3;
(CircleMap | [.r,(r + 1).[) . x = CircleMap . x by A1, A2, A9, FUNCT_1:49
.= CircleMap . r by A2, A7, A9, A10, FUNCT_1:49
.= (CircleMap | [.r,(r + 1).[) . r by A8, FUNCT_1:49 ;
then x = r by A1, A2, A9, A8, A6, FUNCT_1:def 4;
hence contradiction by A2, A9, XXREAL_1:4; :: thesis: verum

end;

then not y in {(CircleMap . r)} by TARSKI:def 1;
hence y in the carrier of (Topen_unit_circle (CircleMap . r)) by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;

the carrier of (R^1 | (R^1 ].r,(r + 1).[)) = ].r,(r + 1).[ by PRE_TOPC:8;
hence CircleMap | ].r,(r + 1).[ is Function of (R^1 | (R^1 ].r,(r + 1).[)),(Topen_unit_circle (CircleMap . r)) by A2, A4, FUNCT_2:2; :: thesis: verum