let a be Real; :: thesis: for C being non empty Subset of REAL holds rng ((AffineMap (0,a)) | C) = {a}
let C be non empty Subset of REAL; :: thesis: rng ((AffineMap (0,a)) | C) = {a}
set f = (AffineMap (0,a)) | C;
thus rng ((AffineMap (0,a)) | C) c= {a} :: according to XBOOLE_0:def 10 :: thesis: {a} c= rng ((AffineMap (0,a)) | C)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((AffineMap (0,a)) | C) or y in {a} )
assume y in rng ((AffineMap (0,a)) | C) ; :: thesis: y in {a}
then consider x being object such that
A1: ( x in dom ((AffineMap (0,a)) | C) & y = ((AffineMap (0,a)) | C) . x ) by FUNCT_1:def 3;
reconsider x = x as Real by A1;
y = (AffineMap (0,a)) . x by A1, FUNCT_1:49;
then y = (0 * x) + a by 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)) | C) )
assume a0: y in {a} ; :: thesis: y in rng ((AffineMap (0,a)) | C)
reconsider o = the Element of C as Real ;
C c= REAL ;
then C c= dom (AffineMap (0,a)) by FUNCT_2:def 1;
then a1: dom ((AffineMap (0,a)) | C) = C by RELAT_1:62;
y = (0 * o) + a by a0, TARSKI:def 1
.= (AffineMap (0,a)) . o by FCONT_1:def 4
.= ((AffineMap (0,a)) | C) . o by FUNCT_1:49 ;
hence y in rng ((AffineMap (0,a)) | C) by FUNCT_1:def 3, a1; :: thesis: verum