set X = Topen_unit_circle (CircleMap . r);
set A = ].r,(r + 1).[;
set B = [.r,(r + 1).[;
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 Lm19, RELAT_1:91;
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
set ;
:: 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 assume A6:
y = CircleMap . r
;
:: thesis: contradictionconsider x being
set such that A7:
x in dom (CircleMap | ].r,(r + 1).[)
and A8:
(CircleMap | ].r,(r + 1).[) . x = y
by A5, FUNCT_1:def 5;
r + 0 < r + 1
by XREAL_1:10;
then A9:
r in [.r,(r + 1).[
by XXREAL_1:3;
A10:
dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[
by Lm19, RELAT_1:91;
(CircleMap | [.r,(r + 1).[) . x =
CircleMap . x
by A1, A2, A7, FUNCT_1:72
.=
CircleMap . r
by A2, A6, A7, A8, FUNCT_1:72
.=
(CircleMap | [.r,(r + 1).[) . r
by A9, FUNCT_1:72
;
then
x = r
by A1, A2, A7, A9, A10, FUNCT_1:def 8;
hence
contradiction
by A2, A7, 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:29;
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:4; :: thesis: verum