let a, b be Real; ( a <> 0 implies rng (AffineMap (a,b)) = REAL )
assume A1:
a <> 0
; rng (AffineMap (a,b)) = REAL
thus
rng (AffineMap (a,b)) c= REAL
; XBOOLE_0:def 10 REAL c= rng (AffineMap (a,b))
let e be object ; TARSKI:def 3 ( not e in REAL or e in rng (AffineMap (a,b)) )
assume
e in REAL
; 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))
; verum