let X be LinearTopSpace; :: thesis: for r being non zero Real holds mlt r,X is one-to-one
let r be non zero Real; :: thesis: mlt r,X is one-to-one

now

let x1, x2 be set ; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X & (mlt r,X) . x1 = (mlt r,X) . x2 implies x1 = x2 )
assume that
A1: ( x1 in the carrier of X & x2 in the carrier of X ) and
A2: (mlt r,X) . x1 = (mlt r,X) . x2 ; :: thesis: x1 = x2
reconsider x1' = x1, x2' = x2 as Point of by A1;
( (mlt r,X) . x1 = r * x1' & (mlt r,X) . x2 = r * x2' ) by Def13;
hence x1 = x2 by A2, RLVECT_1:50; :: thesis: verum

end;

hence mlt r,X is one-to-one by FUNCT_2:25; :: thesis: verum