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 )

( ( 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 :: thesis: ( ( for x, y being Element of OAS holds x,f . x '||' y,f . y ) & f <> id the carrier of OAS implies for x being Element of OAS holds not f . x = x )

assume A3:
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 f <> id the carrier of OAS ; :: thesis: for x being Element of OAS holds not f . x = x

then consider y being Element of OAS such that

A4: f . y <> (id the carrier of OAS) . y by FUNCT_2:63;

given x being Element of OAS such that A5: f . x = x ; :: thesis: contradiction

x <> y by A5, A4;

then consider z being Element of OAS such that

A6: not x,y,z are_collinear by DIRAF:37;

x,z '||' f . x,f . z by A1, Th34;

then x,z,f . z are_collinear by A5, DIRAF:def 5;

then A7: z,f . z,x are_collinear by DIRAF:30;

z,f . z,z are_collinear by DIRAF:31;

then A8: z,f . z '||' x,z by A7, DIRAF:34;

A9: f . y <> y by A4;

x,y '||' f . x,f . y by A1, Th34;

then A10: x,y,f . y are_collinear by A5, DIRAF:def 5;

then y,x,f . y are_collinear by DIRAF:30;

then A11: y,x '||' y,f . y by DIRAF:def 5;

A12: y,f . y,x are_collinear by A10, DIRAF:30;

then y,f . y '||' x,z by A13, A8, DIRAF:23;

then y,x '||' x,z by A9, A11, DIRAF:23;

then x,y '||' x,z by DIRAF:22;

hence contradiction by A6, DIRAF:def 5; :: thesis: verum

end;assume f <> id the carrier of OAS ; :: thesis: for x being Element of OAS holds not f . x = x

then consider y being Element of OAS such that

A4: f . y <> (id the carrier of OAS) . y by FUNCT_2:63;

given x being Element of OAS such that A5: f . x = x ; :: thesis: contradiction

x <> y by A5, A4;

then consider z being Element of OAS such that

A6: not x,y,z are_collinear by DIRAF:37;

x,z '||' f . x,f . z by A1, Th34;

then x,z,f . z are_collinear by A5, DIRAF:def 5;

then A7: z,f . z,x are_collinear by DIRAF:30;

z,f . z,z are_collinear by DIRAF:31;

then A8: z,f . z '||' x,z by A7, DIRAF:34;

A9: f . y <> y by A4;

x,y '||' f . x,f . y by A1, Th34;

then A10: x,y,f . y are_collinear by A5, DIRAF:def 5;

then y,x,f . y are_collinear by DIRAF:30;

then A11: y,x '||' y,f . y by DIRAF:def 5;

A12: y,f . y,x are_collinear by A10, DIRAF:30;

A13: now :: thesis: not z = f . z

y,f . y '||' z,f . z
by A3;assume
z = f . z
; :: thesis: contradiction

then z,y '||' z,f . y by A1, Th34;

then z,y,f . y are_collinear by DIRAF:def 5;

then ( y,f . y,y are_collinear & y,f . y,z are_collinear ) by DIRAF:30, DIRAF:31;

hence contradiction by A9, A12, A6, DIRAF:32; :: thesis: verum

end;then z,y '||' z,f . y by A1, Th34;

then z,y,f . y are_collinear by DIRAF:def 5;

then ( y,f . y,y are_collinear & y,f . y,z are_collinear ) by DIRAF:30, DIRAF:31;

hence contradiction by A9, A12, A6, DIRAF:32; :: thesis: verum

then y,f . y '||' x,z by A13, A8, DIRAF:23;

then y,x '||' x,z by A9, A11, DIRAF:23;

then x,y '||' x,z by DIRAF:22;

hence contradiction by A6, DIRAF:def 5; :: thesis: verum

now :: thesis: ( ( f = id the carrier of OAS or for z being Element of OAS holds f . z <> z ) implies for x, y being Element of OAS holds x,f . x '||' y,f . y )

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: verumassume A14:
( 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

A15: x,y '||' f . x,f . y by A1, Th34;

hence x,f . x '||' y,f . y by A14, A16; :: thesis: verum

end;let x, y be Element of OAS; :: thesis: x,f . x '||' y,f . y

A15: x,y '||' f . x,f . y by A1, Th34;

A16: now :: thesis: ( ( for z being Element of OAS holds f . z <> z ) implies x,f . x '||' y,f . y )

( f = id the carrier of OAS implies x,f . x '||' y,f . y )
by DIRAF:20;assume A17:
for z being Element of OAS 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 OAS such that

A19: x,f . x,z are_collinear and

A20: y,f . y,z are_collinear by A15, Th48;

set t = f . z;

x,f . x,f . z are_collinear by A1, A19, Th47;

then A21: x,f . x '||' z,f . z by A19, DIRAF:34;

y,f . y,f . z are_collinear by A1, A20, Th47;

then A22: y,f . y '||' z,f . z by A20, DIRAF:34;

z <> f . z by A17;

hence contradiction by A18, A21, A22, DIRAF:23; :: thesis: verum

end;assume A18: not x,f . x '||' y,f . y ; :: thesis: contradiction

then consider z being Element of OAS such that

A19: x,f . x,z are_collinear and

A20: y,f . y,z are_collinear by A15, Th48;

set t = f . z;

x,f . x,f . z are_collinear by A1, A19, Th47;

then A21: x,f . x '||' z,f . z by A19, DIRAF:34;

y,f . y,f . z are_collinear by A1, A20, Th47;

then A22: y,f . y '||' z,f . z by A20, DIRAF:34;

z <> f . z by A17;

hence contradiction by A18, A21, A22, DIRAF:23; :: thesis: verum

hence x,f . x '||' y,f . y by A14, A16; :: thesis: verum