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 :: thesis: for x1, x2 being object st x1 in the carrier of X & x2 in the carrier of X & (transl (a,X)) . x1 = (transl (a,X)) . x2 holds
x1 = x2
let x1, x2 be object ; :: 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 & x2 in the carrier of X ) and
A2: (transl (a,X)) . x1 = (transl (a,X)) . x2 ; :: thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Point of X by A1;
( (transl (a,X)) . x1 = a + x19 & (transl (a,X)) . x2 = a + x29 ) by Def10;
hence x1 = x2 by A2, RLVECT_1:8; :: thesis: verum
end;
hence transl (a,X) is one-to-one by FUNCT_2:19; :: thesis: verum