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 )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