let a be Real; rng (AffineMap (0,a)) = {a}
set f = AffineMap (0,a);
thus
rng (AffineMap (0,a)) c= {a}
XBOOLE_0:def 10 {a} c= rng (AffineMap (0,a))
let y be object ; TARSKI:def 3 ( not y in {a} or y in rng (AffineMap (0,a)) )
assume a0:
y in {a}
; y in rng (AffineMap (0,a))
0 in REAL
by XREAL_0:def 1;
then A1:
0 in dom (AffineMap (0,a))
by FUNCT_2:def 1;
y =
(0 * 0) + a
by a0, TARSKI:def 1
.=
(AffineMap (0,a)) . 0
by FCONT_1:def 4
;
hence
y in rng (AffineMap (0,a))
by FUNCT_1:def 3, A1; verum