let a be Real; for C being non empty Subset of REAL holds rng ((AffineMap (0,a)) | C) = {a}
let C be non empty Subset of REAL; rng ((AffineMap (0,a)) | C) = {a}
set f = (AffineMap (0,a)) | C;
thus
rng ((AffineMap (0,a)) | C) c= {a}
XBOOLE_0:def 10 {a} c= rng ((AffineMap (0,a)) | C)
let y be object ; TARSKI:def 3 ( not y in {a} or y in rng ((AffineMap (0,a)) | C) )
assume a0:
y in {a}
; 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; verum