let AFP be AffinPlane; for a, x, y being Element of AFP
for f being Permutation of the carrier of AFP st f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y holds
y = f . x
let a, x, y be Element of AFP; for f being Permutation of the carrier of AFP st f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y holds
y = f . x
let f be Permutation of the carrier of AFP; ( f is translation & not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y implies y = f . x )
assume A1:
f is translation
; ( LIN a,f . a,x or not a,f . a // x,y or not a,x // f . a,y or y = f . x )
then A2:
f is dilatation
by TRANSGEO:def 11;
then A3:
a,x // f . a,f . x
by TRANSGEO:68;
assume A4:
( not LIN a,f . a,x & a,f . a // x,y & a,x // f . a,y )
; y = f . x
a,f . a // x,f . x
by A1, A2, TRANSGEO:82;
hence
y = f . x
by A4, A3, TRANSGEO:80; verum