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

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