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

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