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 ;
TARSKI:def 3 ( 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).[)
;
y in the carrier of (Topen_unit_circle (CircleMap . r))
now not y = CircleMap . rA6:
dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[
by Lm18, RELAT_1:62;
assume A7:
y = CircleMap . r
;
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;
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;
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; verum