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

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

A5: now

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

now

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

proof

assume LIN a,z,x ; :: thesis: contradiction
then A10: LIN a,x,z by DIRAF:30;
( LIN a,x,a & LIN a,x,b ) 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, Th63;
hence f . x = x by A1, A2, A9, Th63; :: thesis: verum

end;

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

end;

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

end;

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