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

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