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, Lm52, FUNCT_1:49
.= ((1 / (2 * PI)) * x) + 1 by FCONT_1:def 4
.= (x / (2 * PI)) + 1 by XCMPLX_1:99 ;
then reconsider y = y as Real ;
x < PI by A1, Lm52, 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 A4: (x / (2 * PI)) + 1 < (1 / 2) + 1 by XREAL_1:6;
0 <= x by A1, Lm52, XXREAL_1:3;
then 0 + 1 <= (x / (2 * PI)) + 1 by XREAL_1:6;
then 1 / 2 < y by A3, XXREAL_0:2;
hence y in ].(1 / 2),((1 / 2) + p1).[ by A3, A4, XXREAL_1:4; :: thesis: verum