let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) or y in ].(1 / 2),((1 / 2) + p1).[ )
assume y in rng ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) ; :: thesis: y in ].(1 / 2),((1 / 2) + p1).[
then consider x being object such that
A1: x in dom ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) and
A2: ((AffineMap ((- (1 / (2 * PI))),1)) | (R^1 E)) . x = y by FUNCT_1:def 3;
reconsider x = x as Real by A1;
A3: y = (AffineMap ((- (1 / (2 * PI))),1)) . x by A1, A2, Lm49, FUNCT_1:49
.= ((- (1 / (2 * PI))) * x) + 1 by FCONT_1:def 4
.= (- ((1 / (2 * PI)) * x)) + 1
.= (- (x / (2 * PI))) + 1 by XCMPLX_1:99 ;
then reconsider y = y as Real ;
x < PI by A1, Lm49, XXREAL_1:3;
then x / (2 * PI) < (1 * PI) / (2 * PI) by XREAL_1:74;
then x / (2 * PI) < 1 / 2 by XCMPLX_1:91;
then - (x / (2 * PI)) > - (1 / 2) by XREAL_1:24;
then A4: (- (x / (2 * PI))) + 1 > (- (1 / 2)) + 1 by XREAL_1:6;
0 <= x by A1, Lm49, XXREAL_1:3;
then 0 + 1 >= (- (x / (2 * PI))) + 1 by XREAL_1:6;
then y < 3 / 2 by A3, XXREAL_0:2;
hence y in ].(1 / 2),((1 / 2) + p1).[ by A3, A4, XXREAL_1:4; :: thesis: verum