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 Th35;

now

let x be Point of X; :: thesis: ((transl a,X) " ) . x = (transl (- a),X) . x
consider u being set such that
A2: u in dom (transl a,X) and
A3: x = (transl a,X) . u by A1, FUNCT_1:def 5;
reconsider u = u as Point of X by A2;
A4: x = a + u by A3, Def10;
thus ((transl a,X) " ) . x = ((transl a,X) " ) . x by A1, Lm9, TOPS_2:def 4
.= u by A3, Lm9, FUNCT_2:32
.= (0. X) + u by RLVECT_1:10
.= ((- a) + a) + u by RLVECT_1:16
.= (- a) + x by A4, RLVECT_1:def 6
.= (transl (- a),X) . x by Def10 ; :: thesis: verum

end;

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