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