let OAS be OAffinSpace; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation holds
for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation implies for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) )
assume A1: f is dilatation ; :: thesis: for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
let a, b, c, d be Element of OAS; :: thesis: ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
A2: a,b '||' f . a,f . b by A1, Th51;
A3: c,d '||' f . c,f . d by A1, Th51;

A4: now

assume a,b '||' c,d ; :: thesis: f . a,f . b '||' f . c,f . d
then A5: ( f . a,f . b '||' c,d or a = b ) by A2, DIRAF:28;

now

assume A6: f . a,f . b '||' c,d ; :: thesis: f . a,f . b '||' f . c,f . d
( c = d implies f . a,f . b '||' f . c,f . d ) by DIRAF:25;
hence f . a,f . b '||' f . c,f . d by A3, A6, DIRAF:28; :: thesis: verum

end;

hence f . a,f . b '||' f . c,f . d by A5, DIRAF:25; :: thesis: verum

end;

now

assume A7: f . a,f . b '||' f . c,f . d ; :: thesis: a,b '||' c,d

A8: now

assume f . a = f . b ; :: thesis: a,b '||' c,d
then a = b by FUNCT_2:85;
hence a,b '||' c,d by DIRAF:25; :: thesis: verum

end;

now

assume A9: a,b '||' f . c,f . d ; :: thesis: a,b '||' c,d

now

assume f . c = f . d ; :: thesis: a,b '||' c,d
then c = d by FUNCT_2:85;
hence a,b '||' c,d by DIRAF:25; :: thesis: verum

end;

hence a,b '||' c,d by A3, A9, DIRAF:28; :: thesis: verum

end;

hence a,b '||' c,d by A2, A7, A8, DIRAF:28; :: thesis: verum

end;

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