let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in K112((CircleMap | [.r,(r + 1).[)) or not y in K112((CircleMap | [.r,(r + 1).[)) or not (CircleMap | [.r,(r + 1).[) . x = (CircleMap | [.r,(r + 1).[) . y or x = y )

set g = CircleMap | [.0,1.[;

set f = CircleMap | [.r,(r + 1).[;

assume that

A1: x in dom (CircleMap | [.r,(r + 1).[) and

A2: y in dom (CircleMap | [.r,(r + 1).[) and

A3: (CircleMap | [.r,(r + 1).[) . x = (CircleMap | [.r,(r + 1).[) . y ; :: thesis: x = y

A4: dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[ by Lm18, RELAT_1:62;

reconsider x = x, y = y as Real by A1, A2;

A5: dom (CircleMap | [.0,1.[) = [.0,1.[ by Lm18, RELAT_1:62;

A6: r <= y by A4, A2, XXREAL_1:3;

A7: x < r + 1 by A4, A1, XXREAL_1:3;

set x1 = frac x;

A8: frac x = x - [\x/] by INT_1:def 8;

A9: frac x < 1 by INT_1:43;

0 <= frac x by INT_1:43;

then A10: frac x in [.0,1.[ by A9, XXREAL_1:3;

set y1 = frac y;

A11: frac y = y - [\y/] by INT_1:def 8;

A12: frac y < 1 by INT_1:43;

0 <= frac y by INT_1:43;

then A13: frac y in [.0,1.[ by A12, XXREAL_1:3;

A14: (CircleMap | [.r,(r + 1).[) . y = CircleMap . y by A2, FUNCT_1:47

.= CircleMap . (y + (- [\y/])) by Th31

.= (CircleMap | [.0,1.[) . (frac y) by A5, A11, A13, FUNCT_1:47 ;

(CircleMap | [.r,(r + 1).[) . x = CircleMap . x by A1, FUNCT_1:47

.= CircleMap . (x + (- [\x/])) by Th31

.= (CircleMap | [.0,1.[) . (frac x) by A5, A8, A10, FUNCT_1:47 ;

then A15: frac x = frac y by A5, A3, A10, A13, A14, Lm23;

A16: y < r + 1 by A4, A2, XXREAL_1:3;

r <= x by A4, A1, XXREAL_1:3;

hence x = y by A7, A6, A16, A15, INT_1:72; :: thesis: verum

set g = CircleMap | [.0,1.[;

set f = CircleMap | [.r,(r + 1).[;

assume that

A1: x in dom (CircleMap | [.r,(r + 1).[) and

A2: y in dom (CircleMap | [.r,(r + 1).[) and

A3: (CircleMap | [.r,(r + 1).[) . x = (CircleMap | [.r,(r + 1).[) . y ; :: thesis: x = y

A4: dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[ by Lm18, RELAT_1:62;

reconsider x = x, y = y as Real by A1, A2;

A5: dom (CircleMap | [.0,1.[) = [.0,1.[ by Lm18, RELAT_1:62;

A6: r <= y by A4, A2, XXREAL_1:3;

A7: x < r + 1 by A4, A1, XXREAL_1:3;

set x1 = frac x;

A8: frac x = x - [\x/] by INT_1:def 8;

A9: frac x < 1 by INT_1:43;

0 <= frac x by INT_1:43;

then A10: frac x in [.0,1.[ by A9, XXREAL_1:3;

set y1 = frac y;

A11: frac y = y - [\y/] by INT_1:def 8;

A12: frac y < 1 by INT_1:43;

0 <= frac y by INT_1:43;

then A13: frac y in [.0,1.[ by A12, XXREAL_1:3;

A14: (CircleMap | [.r,(r + 1).[) . y = CircleMap . y by A2, FUNCT_1:47

.= CircleMap . (y + (- [\y/])) by Th31

.= (CircleMap | [.0,1.[) . (frac y) by A5, A11, A13, FUNCT_1:47 ;

(CircleMap | [.r,(r + 1).[) . x = CircleMap . x by A1, FUNCT_1:47

.= CircleMap . (x + (- [\x/])) by Th31

.= (CircleMap | [.0,1.[) . (frac x) by A5, A8, A10, FUNCT_1:47 ;

then A15: frac x = frac y by A5, A3, A10, A13, A14, Lm23;

A16: y < r + 1 by A4, A2, XXREAL_1:3;

r <= x by A4, A1, XXREAL_1:3;

hence x = y by A7, A6, A16, A15, INT_1:72; :: thesis: verum