let y be object ; :: 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 object 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 3;
reconsider x = x as Real by A1;
0 < x by A1, Lm33, XXREAL_1:4;
then A3: 1 - x < 1 - 0 by XREAL_1:15;
x < 1 by A1, Lm33, XXREAL_1:4;
then A4: 1 - 1 < 1 - x by XREAL_1:15;
y = (AffineMap ((- 1),1)) . x by A1, A2, Lm33, FUNCT_1:49
.= ((- 1) * x) + 1 by FCONT_1:def 4 ;
hence y in ].0,1.[ by A4, A3, XXREAL_1:4; :: thesis: verum