let a, r be real number ; :: 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:91;
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 set ; :: 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 set 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 5;
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:11;
x < (r + a) + 1 by A1, A2, XXREAL_1:4;
then A5: x - a < ((r + a) + 1) - a by XREAL_1:11;
y = (AffineMap 1,(- a)) . x by A2, A3, FUNCT_1:70
.= (1 * x) + (- a) by JORDAN16:def 3 ;
hence y in ].r,(r + 1).[ by A4, A5, XXREAL_1:4; :: thesis: verum

end;

let y be set ; :: 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 A6, XXREAL_1:4;
then A7: y + a < (r + 1) + a by XREAL_1:8;
r < y by A6, XXREAL_1:4;
then r + a < y + a by XREAL_1:8;
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:72
.= (1 * (y + a)) + (- a) by JORDAN16:def 3
.= y ;
hence y in rng ((AffineMap 1,(- a)) | ].(r + a),((r + a) + 1).[) by A1, A8, FUNCT_1:def 5; :: thesis: verum

end;