let a, b be real number ; :: 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:156, ZFMISC_1:92; :: 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 set ; :: 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:116;
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:8;
then A8: (x + i) - n < ((b + n) + i) - n by XREAL_1:11;
set k = (x + i) - n;
A9: CircleMap . ((x + i) - n) = CircleMap . (x + (i - n))
.= y by A4, Th32 ;
A10: (x + i) - n in the carrier of R^1 by TOPMETR:24, XREAL_0:def 1;
a + n < x by A5, A7, XXREAL_1:4;
then (a + n) + i < x + i by XREAL_1:8;
then ((a + n) + i) - n < (x + i) - n by XREAL_1:11;
then (x + i) - n in d by A2, A8, XXREAL_1:4;
hence y in CircleMap .: d by A10, A9, FUNCT_2:43; :: thesis: verum