let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((R^1 (AffineMap (- 1),1)) | (R^1 ].0 ,1.[)) or y in ].0 ,1.[ )
assume y in rng ((R^1 (AffineMap (- 1),1)) | (R^1 ].0 ,1.[)) ; :: thesis: y in ].0 ,1.[
then consider x being set such that
A1: x in dom ((R^1 (AffineMap (- 1),1)) | (R^1 ].0 ,1.[)) and
A2: ((R^1 (AffineMap (- 1),1)) | (R^1 ].0 ,1.[)) . x = y by FUNCT_1:def 5;
reconsider x = x as Real by A1, Lm33;
0 < x by A1, Lm33, XXREAL_1:4;
then A3: 1 - x < 1 - 0 by XREAL_1:17;
x < 1 by A1, Lm33, XXREAL_1:4;
then A4: 1 - 1 < 1 - x by XREAL_1:17;
y = (AffineMap (- 1),1) . x by A1, A2, Lm33, FUNCT_1:72
.= ((- 1) * x) + 1 by JORDAN16:def 3 ;
hence y in ].0 ,1.[ by A4, A3, XXREAL_1:4; :: thesis: verum