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: c,d // f . c,f . d by A1, Th68;
A3: a,b // f . a,f . b by A1, Th68;

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 AFF_1:3; :: thesis: verum

end;

assume a,b // f . c,f . d ; :: thesis: a,b // c,d
hence a,b // c,d by A2, A6, AFF_1:5; :: 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 AFF_1:3; :: thesis: verum

end;

assume f . a,f . b // f . c,f . d ; :: thesis: a,b // c,d
hence a,b // c,d by A3, A7, A5, AFF_1:5; :: 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 AFF_1:3;
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 A2, A9, AFF_1:5; :: 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 A3, AFF_1:5;
hence f . a,f . b // f . c,f . d by A8, AFF_1:3; :: thesis: verum

end;

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