let x, y be object ; FUNCT_1:def 4 ( not x in K113((CircleMap | [.r,(r + 1).[)) or not y in K113((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
; 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; verum