let a, b be Real; :: thesis: for d being set st d in IntIntervals (a,b) holds
CircleMap .: d = CircleMap .: (union (IntIntervals (a,b)))
set D = IntIntervals (a,b);
let d be set ; :: thesis: ( d in IntIntervals (a,b) implies CircleMap .: d = CircleMap .: (union (IntIntervals (a,b))) )
assume A1: d in IntIntervals (a,b) ; :: thesis: CircleMap .: d = CircleMap .: (union (IntIntervals (a,b)))
hence CircleMap .: d c= CircleMap .: (union (IntIntervals (a,b))) by RELAT_1:123, ZFMISC_1:74; :: according to XBOOLE_0:def 10 :: thesis: CircleMap .: (union (IntIntervals (a,b))) c= CircleMap .: d
consider i being Element of INT such that
A2: d = ].(a + i),(b + i).[ by A1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in CircleMap .: (union (IntIntervals (a,b))) or y in CircleMap .: d )
assume y in CircleMap .: (union (IntIntervals (a,b))) ; :: thesis: y in CircleMap .: d
then consider x being Element of R^1 such that
A3: x in union (IntIntervals (a,b)) and
A4: y = CircleMap . x by FUNCT_2:65;
consider Z being set such that
A5: x in Z and
A6: Z in IntIntervals (a,b) by A3, TARSKI:def 4;
consider n being Element of INT such that
A7: Z = ].(a + n),(b + n).[ by A6;
x < b + n by A5, A7, XXREAL_1:4;
then x + i < (b + n) + i by XREAL_1:6;
then A8: (x + i) - n < ((b + n) + i) - n by XREAL_1:9;
set k = (x + i) - n;
A9: CircleMap . ((x + i) - n) = CircleMap . (x + (i - n))
.= y by A4, Th31 ;
A10: (x + i) - n in the carrier of R^1 by TOPMETR:17, XREAL_0:def 1;
a + n < x by A5, A7, XXREAL_1:4;
then (a + n) + i < x + i by XREAL_1:6;
then ((a + n) + i) - n < (x + i) - n by XREAL_1:9;
then (x + i) - n in d by A2, A8, XXREAL_1:4;
hence y in CircleMap .: d by A10, A9, FUNCT_2:35; :: thesis: verum