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

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