let y be object ; TARSKI:def 3 ( 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.[))
; 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; verum