let OAS be OAffinSpace; :: thesis: for a being Element of OAS
for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds
f = g

let a be Element of OAS; :: thesis: for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds
f = g

let f, g be Permutation of the carrier of OAS; :: thesis: ( f is translation & g is translation & f . a = g . a implies f = g )
assume that
A1: f is translation and
A2: g is translation and
A3: f . a = g . a ; :: thesis: f = g
set b = f . a;
A4: f is dilatation by A1;
A5: now :: thesis: ( a <> f . a implies f = g )
assume A6: a <> f . a ; :: thesis: f = g
for x being Element of OAS holds f . x = g . x
proof
let x be Element of OAS; :: thesis: f . x = g . x
now :: thesis: ( a,f . a,x are_collinear implies f . x = g . x )
assume A7: a,f . a,x are_collinear ; :: thesis: f . x = g . x
now :: thesis: ( x <> a implies f . x = g . x )end;
hence f . x = g . x by A3; :: thesis: verum
end;
hence f . x = g . x by A1, A2, A3, Th54; :: thesis: verum
end;
hence f = g by FUNCT_2:63; :: thesis: verum
end;
( f . a = a implies f = g ) by A1, A2, A3;
hence f = g by A5; :: thesis: verum