let a, b be real number ; :: thesis: ( a <> 0 implies rng (AffineMap a,b) = REAL )
assume A1: a <> 0 ; :: thesis: rng (AffineMap a,b) = REAL
thus rng (AffineMap a,b) c= REAL ; :: according to XBOOLE_0:def 10 :: thesis: REAL c= rng (AffineMap a,b)
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in REAL or e in rng (AffineMap a,b) )
assume e in REAL ; :: thesis: e in rng (AffineMap a,b)
then reconsider r = e as Element of REAL ;
set s = (r - b) / a;
(AffineMap a,b) . ((r - b) / a) = (a * ((r - b) / a)) + b by Def3
.= (r - b) + b by A1, XCMPLX_1:88
.= r ;
hence e in rng (AffineMap a,b) by FUNCT_2:6; :: thesis: verum