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:87
.= r ;
hence e in rng (AffineMap (a,b)) by FUNCT_2:4; :: thesis: verum