let OAS be OAffinSpace; :: thesis:
let f be Permutation of the carrier of OAS; :: thesis:
assume A1: f is dilatation ; :: thesis:
let a, b, c, d be Element of OAS; :: thesis:
A2: c,d '||' f . c,f . d by A1, Th34;
A3: a,b '||' f . a,f . b by A1, Th34;

A4: now :: thesis:

A5: now :: thesis:

A6: now :: thesis:

assume f . c = f . d ; :: thesis:
then c = d by FUNCT_2:58;
hence a,b '||' c,d by DIRAF:20; :: thesis:

end;

assume a,b '||' f . c,f . d ; :: thesis:
hence a,b '||' c,d by A2, A6, DIRAF:23; :: thesis:

end;

A7: now :: thesis:

assume f . a = f . b ; :: thesis:
then a = b by FUNCT_2:58;
hence a,b '||' c,d by DIRAF:20; :: thesis:

end;

assume f . a,f . b '||' f . c,f . d ; :: thesis:
hence a,b '||' c,d by A3, A7, A5, DIRAF:23; :: thesis:

end;

now :: thesis:

A8: now :: thesis:

A9: ( c = d implies f . a,f . b '||' f . c,f . d ) by DIRAF:20;
assume f . a,f . b '||' c,d ; :: thesis:
hence f . a,f . b '||' f . c,f . d by A2, A9, DIRAF:23; :: thesis:

end;

assume a,b '||' c,d ; :: thesis:
then ( f . a,f . b '||' c,d or a = b ) by A3, DIRAF:23;
hence f . a,f . b '||' f . c,f . d by A8, DIRAF:20; :: thesis:

end;

hence ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) by A4; :: thesis: