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
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
A2: x in union (IntIntervals a,b) and
A3: y = CircleMap . x by FUNCT_2:116;
consider Z being set such that
A4: x in Z and
A5: Z in IntIntervals a,b by A2, TARSKI:def 4;
consider n being Element of INT such that
A6: Z = ].(a + n),(b + n).[ by A5;
consider i being Element of INT such that
A7: d = ].(a + i),(b + i).[ by A1;
set k = (x + i) - n;
A8: (x + i) - n in the carrier of R^1 by TOPMETR:24, XREAL_0:def 1;
( a + n < x & x < b + n ) by A4, A6, XXREAL_1:4;
then ( (a + n) + i < x + i & x + i < (b + n) + i ) by XREAL_1:8;
then ( ((a + n) + i) - n < (x + i) - n & (x + i) - n < ((b + n) + i) - n ) by XREAL_1:11;
then A9: (x + i) - n in d by A7, XXREAL_1:4;
CircleMap . ((x + i) - n) = CircleMap . (x + (i - n))
.= y by A3, Th32 ;
hence y in CircleMap .: d by A8, A9, FUNCT_2:43; :: thesis: verum