let OAS be OAffinSpace; for f being Permutation of the carrier of OAS st f is translation holds
f " is translation
let f be Permutation of the carrier of OAS; ( f is translation implies f " is translation )
A1:
now ( ( for x being Element of OAS holds f . x <> x ) implies for y being Element of OAS holds not (f ") . y = y )assume A2:
for
x being
Element of
OAS holds
f . x <> x
;
for y being Element of OAS holds not (f ") . y = ygiven y being
Element of
OAS such that A3:
(f ") . y = y
;
contradiction
f . y = y
by A3, Th2;
hence
contradiction
by A2;
verum end;
assume A4:
f is translation
; f " is translation
then
f is dilatation
;
then A5:
f " is dilatation
by Th43;
( f = id the carrier of OAS implies f " = id the carrier of OAS )
by FUNCT_1:45;
hence
f " is translation
by A4, A5, A1; verum