let AFS be AffinSpace; for a, b being Element of AFS
for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds
f = g
let a, b be Element of AFS; for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds
f = g
let f, g be Permutation of the carrier of AFS; ( f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b implies f = g )
assume that
A1:
f is dilatation
and
A2:
g is dilatation
and
A3:
f . a = g . a
and
A4:
f . b = g . b
; ( a = b or f = g )
A5: ((g ") * f) . b =
(g ") . (g . b)
by A4, FUNCT_2:15
.=
b
by Th2
;
A6:
g " is dilatation
by A2, Th70;
assume A7:
a <> b
; f = g
((g ") * f) . a =
(g ") . (g . a)
by A3, FUNCT_2:15
.=
a
by Th2
;
then A8:
(g ") * f = id the carrier of AFS
by A1, A7, A5, A6, Th71, Th78;
hence
f = g
by FUNCT_2:63; verum