let y be set ; :: 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 set 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 5;
reconsider x = x as Real by A1;
A3: y = (AffineMap (1 / (2 * PI )),0 ) . x by A1, A2, Lm28, FUNCT_1:72
.= ((1 / (2 * PI )) * x) + 0 by JORDAN16:def 3
.= x / (2 * PI ) by XCMPLX_1:100 ;
then reconsider y = y as Real ;
x <= PI by A1, Lm28, XXREAL_1:2;
then y <= (1 * PI ) / (2 * PI ) by A3, XREAL_1:74;
then y <= 1 / 2 by XCMPLX_1:92;
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