let OAS be OAffinSpace; :: thesis: for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of OAS
let a, b be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds
f = id the carrier of OAS
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . a = a & f . b = b & a <> b implies f = id the carrier of OAS )
assume that
A1: f is dilatation and
A2: f . a = a and
A3: f . b = b and
A4: a <> b ; :: thesis: f = id the carrier of OAS

now :: thesis: for x being Element of OAS holds f . x = (id the carrier of OAS) . x

let x be Element of OAS; :: thesis: f . x = (id the carrier of OAS) . x

A5: now :: thesis: ( a,b,x are_collinear implies f . x = x )

assume A6: a,b,x are_collinear ; :: thesis: f . x = x

now :: thesis: ( x <> a implies f . x = x )

consider z being Element of OAS such that
A7: not a,b,z are_collinear by A4, DIRAF:37;
assume A8: x <> a ; :: thesis: f . x = x
A9: not a,z,x are_collinear

proof

assume a,z,x are_collinear ; :: thesis: contradiction
then A10: a,x,z are_collinear by DIRAF:30;
( a,x,a are_collinear & a,x,b are_collinear ) by A6, DIRAF:30, DIRAF:31;
hence contradiction by A8, A7, A10, DIRAF:32; :: thesis: verum

end;

f . z = z by A1, A2, A3, A7, Th50;
hence f . x = x by A1, A2, A9, Th50; :: thesis: verum

end;

hence f . x = x by A2; :: thesis: verum

end;

( not a,b,x are_collinear implies f . x = x ) by A1, A2, A3, Th50;
hence f . x = (id the carrier of OAS) . x by A5; :: thesis: verum

end;

hence f = id the carrier of OAS by FUNCT_2:63; :: thesis: verum