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 set ; :: 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 6
.= (0. X) + y by RLVECT_1:16
.= y by RLVECT_1:10 ;
hence y in rng (transl a,X) by FUNCT_2:6; :: thesis: verum