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

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

let f, g be Permutation of the carrier of AFS; :: 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 AFS holds f . x = g . x
proof
let x be Element of AFS; :: thesis: f . x = g . x
now :: thesis: ( LIN a,f . a,x implies f . x = g . x )
assume A7: LIN a,f . a,x ; :: thesis: f . x = g . x
now :: thesis: ( x <> a implies f . x = g . x )
A8: f <> id the carrier of AFS by A6;
then A9: f . x <> x by A1;
assume x <> a ; :: thesis: f . x = g . x
consider p being Element of AFS such that
A10: not LIN a,f . a,p by ;
A11: f . p <> p by A1, A8;
A12: not LIN p,f . p,x
proof
A13: LIN a,f . a,f . x by A4, A7, Th74;
LIN a,f . a,a by AFF_1:7;
then A14: LIN x,f . x,a by ;
A15: LIN p,f . p,p by AFF_1:7;
LIN a,f . a,f . a by AFF_1:7;
then A16: LIN x,f . x,f . a by ;
assume A17: LIN p,f . p,x ; :: thesis: contradiction
then LIN p,f . p,f . x by ;
then LIN x,f . x,p by ;
hence contradiction by A10, A9, A14, A16, AFF_1:8; :: thesis: verum
end;
f . p = g . p by A1, A2, A3, A10, Th83;
hence f . x = g . x by A1, A2, A12, Th83; :: thesis: verum
end;
hence f . x = g . x by A3; :: thesis: verum
end;
hence f . x = g . x by A1, A2, A3, Th83; :: 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