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 & f . b = b & 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
A3: ( not LIN a,b,x implies f . x = x ) by A1, A2, Th63;

now

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

now

assume A5: x <> a ; :: thesis: f . x = x
consider z being Element of OAS such that
A6: not LIN a,b,z by A2, DIRAF:43;
A7: f . z = z by A1, A2, A6, Th63;
not LIN a,z,x

proof

assume LIN a,z,x ; :: thesis: contradiction
then ( LIN a,x,a & LIN a,x,z & LIN a,x,b ) by A4, DIRAF:36, DIRAF:37;
hence contradiction by A5, A6, DIRAF:38; :: thesis: verum

end;

hence f . x = x by A1, A2, A7, Th63; :: thesis: verum

end;

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

end;

hence f . x = (id the carrier of OAS) . x by A3, FUNCT_1:35; :: thesis: verum

end;

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