let a be Real; :: thesis: rng (AffineMap (0,a)) = {a}
set f = AffineMap (0,a);
thus rng (AffineMap (0,a)) c= {a} :: according to XBOOLE_0:def 10 :: thesis: {a} c= rng (AffineMap (0,a))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (AffineMap (0,a)) or y in {a} )
assume y in rng (AffineMap (0,a)) ; :: thesis: y in {a}
then consider x being object such that
A1: ( x in dom (AffineMap (0,a)) & y = (AffineMap (0,a)) . x ) by FUNCT_1:def 3;
reconsider x = x as Real by A1;
y = (0 * x) + a by A1, FCONT_1:def 4
.= a ;
hence y in {a} by TARSKI:def 1; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {a} or y in rng (AffineMap (0,a)) )
assume a0: y in {a} ; :: thesis: 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; :: thesis: verum