let X be LinearTopSpace; :: thesis: for a being Point of X holds rng (transl (a,X)) = [#] X
let a be Point of X; :: thesis: rng (transl (a,X)) = [#] X
thus rng (transl (a,X)) c= [#] X ; :: according to XBOOLE_0:def 10 :: thesis: [#] X c= rng (transl (a,X))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] X or y in rng (transl (a,X)) )
assume y in [#] X ; :: thesis: y in rng (transl (a,X))
then reconsider y = y as Point of X ;
(transl (a,X)) . ((- a) + y) = a + ((- a) + y) by Def10
.= (a + (- a)) + y by RLVECT_1:def 3
.= (0. X) + y by RLVECT_1:5
.= y ;
hence y in rng (transl (a,X)) by FUNCT_2:4; :: thesis: verum