let X be LinearTopSpace; :: thesis: for a being Point of X holds transl a,X is one-to-one
let a be Point of X; :: thesis: transl a,X is one-to-one

now

let x1, x2 be set ; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X & (transl a,X) . x1 = (transl a,X) . x2 implies x1 = x2 )
assume that
A1: x1 in the carrier of X and
A2: x2 in the carrier of X and
A3: (transl a,X) . x1 = (transl a,X) . x2 ; :: thesis: x1 = x2
reconsider x1' = x1, x2' = x2 as Point of X by A1, A2;
( (transl a,X) . x1 = a + x1' & (transl a,X) . x2 = a + x2' ) by Def10;
hence x1 = x2 by A3, RLVECT_1:21; :: thesis: verum

end;

hence transl a,X is one-to-one by FUNCT_2:25; :: thesis: verum