let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS st f is dilatation holds
for a, b, c, d being Element of AFS holds
( a,b // c,d iff f . a,f . b // f . c,f . d )
let f be Permutation of the carrier of AFS; :: thesis: ( f is dilatation implies for a, b, c, d being Element of AFS 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 AFS holds
( a,b // c,d iff f . a,f . b // f . c,f . d )
let a, b, c, d be Element of AFS; :: thesis: ( a,b // c,d iff f . a,f . b // f . c,f . d )
A2: a,b // f . a,f . b by A1, Th85;
A3: c,d // f . c,f . d by A1, Th85;

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, AFF_1:14;

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 AFF_1:12;
hence f . a,f . b // f . c,f . d by A3, A6, AFF_1:14; :: thesis: verum

end;

hence f . a,f . b // f . c,f . d by A5, AFF_1:12; :: 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 AFF_1:12; :: 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 AFF_1:12; :: thesis: verum

end;

hence a,b // c,d by A3, A9, AFF_1:14; :: thesis: verum

end;

hence a,b // c,d by A2, A7, A8, AFF_1:14; :: thesis: verum

end;

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