let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation holds
( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y )

let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation implies ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) )
assume A1: f is dilatation ; :: thesis: ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y )
A2: now :: thesis: ( ( for x, y being Element of AFS holds x,f . x // y,f . y ) & f <> id the carrier of AFS implies for x being Element of AFS holds not f . x = x )
assume A3: for x, y being Element of AFS holds x,f . x // y,f . y ; :: thesis: ( f <> id the carrier of AFS implies for x being Element of AFS holds not f . x = x )
assume f <> id the carrier of AFS ; :: thesis: for x being Element of AFS holds not f . x = x
then consider y being Element of AFS such that
A4: f . y <> (id the carrier of AFS) . y by FUNCT_2:63;
given x being Element of AFS such that A5: f . x = x ; :: thesis: contradiction
x <> y by A5, A4;
then consider z being Element of AFS such that
A6: not LIN x,y,z by AFF_1:13;
x,z // f . x,f . z by ;
then LIN x,z,f . z by ;
then A7: LIN z,f . z,x by AFF_1:6;
LIN z,f . z,z by AFF_1:7;
then A8: z,f . z // x,z by ;
A9: f . y <> y by A4;
x,y // f . x,f . y by ;
then A10: LIN x,y,f . y by ;
then LIN y,x,f . y by AFF_1:6;
then A11: y,x // y,f . y by AFF_1:def 1;
A12: LIN y,f . y,x by ;
A13: now :: thesis: not z = f . z
assume z = f . z ; :: thesis: contradiction
then z,y // z,f . y by ;
then LIN z,y,f . y by AFF_1:def 1;
then ( LIN y,f . y,y & LIN y,f . y,z ) by ;
hence contradiction by A9, A12, A6, AFF_1:8; :: thesis: verum
end;
y,f . y // z,f . z by A3;
then y,f . y // x,z by ;
then y,x // x,z by ;
then x,y // x,z by AFF_1:4;
hence contradiction by A6, AFF_1:def 1; :: thesis: verum
end;
now :: thesis: ( ( f = id the carrier of AFS or for z being Element of AFS holds f . z <> z ) implies for x, y being Element of AFS holds x,f . x // y,f . y )
assume A14: ( f = id the carrier of AFS or for z being Element of AFS holds f . z <> z ) ; :: thesis: for x, y being Element of AFS holds x,f . x // y,f . y
let x, y be Element of AFS; :: thesis: x,f . x // y,f . y
A15: x,y // f . x,f . y by ;
A16: now :: thesis: ( ( for z being Element of AFS holds f . z <> z ) implies x,f . x // y,f . y )
assume A17: for z being Element of AFS holds f . z <> z ; :: thesis: x,f . x // y,f . y
assume A18: not x,f . x // y,f . y ; :: thesis: contradiction
then consider z being Element of AFS such that
A19: LIN x,f . x,z and
A20: LIN y,f . y,z by ;
set t = f . z;
LIN x,f . x,f . z by ;
then A21: x,f . x // z,f . z by ;
LIN y,f . y,f . z by ;
then A22: y,f . y // z,f . z by ;
z <> f . z by A17;
hence contradiction by A18, A21, A22, AFF_1:5; :: thesis: verum
end;
( f = id the carrier of AFS implies x,f . x // y,f . y ) by AFF_1:3;
hence x,f . x // y,f . y by ; :: thesis: verum
end;
hence ( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y ) by A2; :: thesis: verum