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 ;
reconsider x = x, y = y as Real by A1, A2;
A5: dom () = [.0,1.[ by ;
A6: r <= y by ;
A7: x < r + 1 by ;
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 ;
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 ;
A14: (CircleMap | [.r,(r + 1).[) . y = CircleMap . y by
.= CircleMap . (y + ()) by Th31
.= () . (frac y) by ;
(CircleMap | [.r,(r + 1).[) . x = CircleMap . x by
.= CircleMap . (x + ()) by Th31
.= () . (frac x) by ;
then A15: frac x = frac y by A5, A3, A10, A13, A14, Lm23;
A16: y < r + 1 by ;
r <= x by ;
hence x = y by ; :: thesis: verum