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