let AFP be AffinPlane; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ) ; :: thesis: y = f . x
a,f . a // x,f . x by A1, A2, TRANSGEO:82;
hence y = f . x by A4, A3, TRANSGEO:80; :: thesis: verum