let X be LinearTopSpace; for a being Point of X holds (transl (a,X)) " = transl ((- a),X)
let a be Point of X; (transl (a,X)) " = transl ((- a),X)
A1:
rng (transl (a,X)) = [#] X
by Th34;
now for x being Point of X holds ((transl (a,X)) ") . x = (transl ((- a),X)) . xlet x be
Point of
X;
((transl (a,X)) ") . x = (transl ((- a),X)) . xconsider 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
;
verum end;
hence
(transl (a,X)) " = transl ((- a),X)
by FUNCT_2:63; verum