let a, b be Real; :: 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 object ; :: 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 ;
reconsider s = (r - b) / a as Element of REAL by XREAL_0:def 1;
(AffineMap (a,b)) . s = (a * s) + b by Def4
.= (r - b) + b by A1, XCMPLX_1:87
.= r ;
then r in rng (AffineMap (a,b)) by FUNCT_2:4;
hence e in rng (AffineMap (a,b)) ; :: thesis: verum