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, Lm35;
A3: y = (AffineMap (- 1),1) . x by A1, A2, Lm35, FUNCT_1:72
.= ((- 1) * x) + 1 by JORDAN16:def 3 ;
( 0 < x & x < 1 ) by A1, Lm35, XXREAL_1:4;
then ( 1 - 1 < 1 - x & 1 - x < 1 - 0 ) by XREAL_1:17;
hence y in ].0 ,1.[ by A3, XXREAL_1:4; :: thesis: verum