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

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