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: c,d '||' f . c,f . d by ;
A3: a,b '||' f . a,f . b by ;
A4: now :: thesis: ( f . a,f . b '||' f . c,f . d implies a,b '||' c,d )
A5: now :: thesis: ( a,b '||' f . c,f . d implies a,b '||' c,d )
A6: now :: thesis: ( f . c = f . d implies a,b '||' c,d )
assume f . c = f . d ; :: thesis: a,b '||' c,d
then c = d by FUNCT_2:58;
hence a,b '||' c,d by DIRAF:20; :: thesis: verum
end;
assume a,b '||' f . c,f . d ; :: thesis: a,b '||' c,d
hence a,b '||' c,d by ; :: thesis: verum
end;
A7: now :: thesis: ( f . a = f . b implies a,b '||' c,d )
assume f . a = f . b ; :: thesis: a,b '||' c,d
then a = b by FUNCT_2:58;
hence a,b '||' c,d by DIRAF:20; :: thesis: verum
end;
assume f . a,f . b '||' f . c,f . d ; :: thesis: a,b '||' c,d
hence a,b '||' c,d by ; :: thesis: verum
end;
now :: thesis: ( a,b '||' c,d implies f . a,f . b '||' f . c,f . d )
A8: now :: thesis: ( f . a,f . b '||' c,d implies f . a,f . b '||' f . c,f . d )
A9: ( c = d implies f . a,f . b '||' f . c,f . d ) by DIRAF:20;
assume f . a,f . b '||' c,d ; :: thesis: f . a,f . b '||' f . c,f . d
hence f . a,f . b '||' f . c,f . d by ; :: thesis: verum
end;
assume a,b '||' c,d ; :: thesis: f . a,f . b '||' f . c,f . d
then ( f . a,f . b '||' c,d or a = b ) by ;
hence f . a,f . b '||' f . c,f . d by ; :: thesis: verum
end;
hence ( a,b '||' c,d iff f . a,f . b '||' f . c,f . d ) by A4; :: thesis: verum