let a, r be Real; :: thesis: rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) = ].r,(r + 1).[
set F = AffineMap (1,(- a));
set f = (AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[;
dom (AffineMap (1,(- a))) = REAL by FUNCT_2:def 1;
then A1: dom ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) = ].(r + a),((r + a) + 1).[ by RELAT_1:62;
thus rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) = ].r,(r + 1).[ :: thesis: verum
proof
thus rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) c= ].r,(r + 1).[ :: according to XBOOLE_0:def 10 :: thesis: ].r,(r + 1).[ c= rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) or y in ].r,(r + 1).[ )
assume y in rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) ; :: thesis: y in ].r,(r + 1).[
then consider x being object such that
A2: x in dom ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) and
A3: ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) . x = y by FUNCT_1:def 3;
reconsider x = x as Real by A2;
r + a < x by ;
then A4: (r + a) - a < x - a by XREAL_1:9;
x < (r + a) + 1 by ;
then A5: x - a < ((r + a) + 1) - a by XREAL_1:9;
y = (AffineMap (1,(- a))) . x by
.= (1 * x) + (- a) by FCONT_1:def 4 ;
hence y in ].r,(r + 1).[ by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ].r,(r + 1).[ or y in rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) )
assume A6: y in ].r,(r + 1).[ ; :: thesis: y in rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[)
then reconsider y = y as Real ;
y < r + 1 by ;
then A7: y + a < (r + 1) + a by XREAL_1:6;
r < y by ;
then r + a < y + a by XREAL_1:6;
then A8: y + a in ].(r + a),((r + a) + 1).[ by ;
then ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) . (y + a) = (AffineMap (1,(- a))) . (y + a) by FUNCT_1:49
.= (1 * (y + a)) + (- a) by FCONT_1:def 4
.= y ;
hence y in rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) by ; :: thesis: verum
end;