let X be LinearTopSpace; :: thesis: for a being Point of X holds (transl (a,X)) " = transl ((- a),X)
let a be Point of X; :: thesis: (transl (a,X)) " = transl ((- a),X)
A1: rng (transl (a,X)) = [#] X by Th34;

now :: thesis: for x being Point of X holds ((transl (a,X)) ") . x = (transl ((- a),X)) . x

let x be Point of X; :: thesis: ((transl (a,X)) ") . x = (transl ((- a),X)) . x
consider u being object such that
A2: u in dom (transl (a,X)) and
A3: x = (transl (a,X)) . u by A1, FUNCT_1:def 3;
reconsider u = u as Point of X by A2;
A4: x = a + u by A3, Def10;
( transl (a,X) is onto & transl (a,X) is one-to-one ) by A1, Lm8, FUNCT_2:def 3;
hence ((transl (a,X)) ") . x = ((transl (a,X)) ") . x by TOPS_2:def 4
.= u by A3, Lm8, FUNCT_2:26
.= (0. X) + u
.= ((- a) + a) + u by RLVECT_1:5
.= (- a) + x by A4, RLVECT_1:def 3
.= (transl ((- a),X)) . x by Def10 ;
:: thesis: verum

end;

hence (transl (a,X)) " = transl ((- a),X) by FUNCT_2:63; :: thesis: verum