set f = CircleMap | [.r,(r + 1).[;
set g = CircleMap | [.0 ,1.[;
A1: dom (CircleMap | [.r,(r + 1).[) = [.r,(r + 1).[ by Lm19, RELAT_1:91;
A2: dom (CircleMap | [.0 ,1.[) = [.0 ,1.[ by Lm19, RELAT_1:91;
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in K1((CircleMap | [.r,(r + 1).[)) or not y in K1((CircleMap | [.r,(r + 1).[)) or not (CircleMap | [.r,(r + 1).[) . x = (CircleMap | [.r,(r + 1).[) . y or x = y )
assume that
A3: x in dom (CircleMap | [.r,(r + 1).[) and
A4: y in dom (CircleMap | [.r,(r + 1).[) and
A5: (CircleMap | [.r,(r + 1).[) . x = (CircleMap | [.r,(r + 1).[) . y ; :: thesis: x = y
reconsider x = x, y = y as Real by A1, A3, A4;
set x1 = frac x;
set y1 = frac y;
A6: frac x = x - [\x/] by INT_1:def 6;
A7: frac y = y - [\y/] by INT_1:def 6;
( 0 <= frac x & frac x < 1 ) by INT_1:69;
then A8: frac x in [.0 ,1.[ by XXREAL_1:3;
( 0 <= frac y & frac y < 1 ) by INT_1:69;
then A9: frac y in [.0 ,1.[ by XXREAL_1:3;
A10: ( r <= x & x < r + 1 ) by A1, A3, XXREAL_1:3;
A11: ( r <= y & y < r + 1 ) by A1, A4, XXREAL_1:3;
A12: (CircleMap | [.r,(r + 1).[) . x = CircleMap . x by A3, FUNCT_1:70
.= CircleMap . (x + (- [\x/])) by Th32
.= (CircleMap | [.0 ,1.[) . (frac x) by A2, A6, A8, FUNCT_1:70 ;
(CircleMap | [.r,(r + 1).[) . y = CircleMap . y by A4, FUNCT_1:70
.= CircleMap . (y + (- [\y/])) by Th32
.= (CircleMap | [.0 ,1.[) . (frac y) by A2, A7, A9, FUNCT_1:70 ;
then frac x = frac y by A2, A5, A8, A9, A12, Lm25, FUNCT_1:def 8;
hence x = y by A10, A11, TOPREALA:7; :: thesis: verum