let a, r be Real; :: thesis:
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:

proof

thus rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) c= ].r,(r + 1).[ :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((AffineMap (1,(- a))) | ].(r + a),((r + a) + 1).[) ; :: thesis:
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 A1, A2, XXREAL_1:4;
then A4: (r + a) - a < x - a by XREAL_1:9;
x < (r + a) + 1 by A1, A2, XXREAL_1:4;
then A5: x - a < ((r + a) + 1) - a by XREAL_1:9;
y = (AffineMap (1,(- a))) . x by A2, A3, FUNCT_1:47
.= (1 * x) + (- a) by FCONT_1:def 4 ;
hence y in ].r,(r + 1).[ by A4, A5, XXREAL_1:4; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: y in ].r,(r + 1).[ ; :: thesis:
then reconsider y = y as Real ;
y < r + 1 by A6, XXREAL_1:4;
then A7: y + a < (r + 1) + a by XREAL_1:6;
r < y by A6, XXREAL_1:4;
then r + a < y + a by XREAL_1:6;
then A8: y + a in ].(r + a),((r + a) + 1).[ by A7, XXREAL_1:4;
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 A1, A8, FUNCT_1:def 3; :: thesis:

end;