let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation holds
( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) )
assume A1: f is dilatation ; :: thesis: ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y )

A2: now

assume A3: ( f = id the carrier of OAS or for z being Element of OAS holds f . z <> z ) ; :: thesis: for x, y being Element of OAS holds x,f . x '||' y,f . y
let x, y be Element of OAS; :: thesis: x,f . x '||' y,f . y
A4: x,y '||' f . x,f . y by A1, Th51;

A5: now

assume f = id the carrier of OAS ; :: thesis: x,f . x '||' y,f . y
then f . y = y by FUNCT_1:35;
hence x,f . x '||' y,f . y by DIRAF:25; :: thesis: verum

end;

now

assume A6: for z being Element of OAS holds f . z <> z ; :: thesis: x,f . x '||' y,f . y
assume A7: not x,f . x '||' y,f . y ; :: thesis: contradiction
then consider z being Element of OAS such that
A8: ( LIN x,f . x,z & LIN y,f . y,z ) by A4, Th61;
set t = f . z;
LIN x,f . x,f . z by A1, A8, Th60;
then A9: x,f . x '||' z,f . z by A8, DIRAF:40;
( LIN y,f . y,z & LIN y,f . y,f . z & y <> f . y ) by A1, A6, A8, Th60;
then y,f . y '||' z,f . z by DIRAF:40;
then ( z <> f . z & z,f . z '||' y,f . y ) by A6, DIRAF:27;
hence contradiction by A7, A9, DIRAF:28; :: thesis: verum

end;

hence x,f . x '||' y,f . y by A3, A5; :: thesis: verum

end;

now

assume A10: for x, y being Element of OAS holds x,f . x '||' y,f . y ; :: thesis: ( f <> id the carrier of OAS implies for x being Element of OAS holds not f . x = x )
assume A11: f <> id the carrier of OAS ; :: thesis: for x being Element of OAS holds not f . x = x
given x being Element of OAS such that A12: f . x = x ; :: thesis: contradiction
consider y being Element of OAS such that
A13: f . y <> (id the carrier of OAS) . y by A11, FUNCT_2:113;
A14: f . y <> y by A13, FUNCT_1:35;
x,y '||' f . x,f . y by A1, Th51;
then A15: LIN x,y,f . y by A12, DIRAF:def 5;
then A16: LIN y,f . y,x by DIRAF:36;
LIN y,x,f . y by A15, DIRAF:36;
then A17: y,x '||' y,f . y by DIRAF:def 5;
x <> y by A12, A13, FUNCT_1:35;
then consider z being Element of OAS such that
A18: not LIN x,y,z by DIRAF:43;
x,z '||' f . x,f . z by A1, Th51;
then LIN x,z,f . z by A12, DIRAF:def 5;
then A19: LIN z,f . z,x by DIRAF:36;

A20: now

assume z = f . z ; :: thesis: contradiction
then z,y '||' z,f . y by A1, Th51;
then LIN z,y,f . y by DIRAF:def 5;
then ( LIN y,f . y,y & LIN y,f . y,z ) by DIRAF:36, DIRAF:37;
hence contradiction by A14, A16, A18, DIRAF:38; :: thesis: verum

end;

LIN z,f . z,z by DIRAF:37;
then A21: z,f . z '||' x,z by A19, DIRAF:40;
y,f . y '||' z,f . z by A10;
then y,f . y '||' x,z by A20, A21, DIRAF:28;
then y,x '||' x,z by A14, A17, DIRAF:28;
then x,y '||' x,z by DIRAF:27;
hence contradiction by A18, DIRAF:def 5; :: thesis: verum

end;

hence ( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y ) by A2; :: thesis: verum