set B = [.r,(r + 1).[;
set A = ].r,(r + 1).[;
set X = Topen_unit_circle ();
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 ;
A3: the carrier of () = the carrier of () \ {()} by Def10;
A4: rng (CircleMap | ].r,(r + 1).[) c= the carrier of ()
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 () )
assume A5: y in rng (CircleMap | ].r,(r + 1).[) ; :: thesis: y in the carrier of ()
now :: thesis: not y = CircleMap . r
A6: dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[ by ;
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 ;
(CircleMap | [.r,(r + 1).[) . x = CircleMap . x by
.= CircleMap . r by
.= (CircleMap | [.r,(r + 1).[) . r by ;
then x = r by ;
hence contradiction by A2, A9, XXREAL_1:4; :: thesis: verum
end;
then not y in {()} by TARSKI:def 1;
hence y in the carrier of () by ; :: 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).[)),() by ; :: thesis: verum