let OAS be OAffinSpace; :: thesis: for a, b being Element of OAS
for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds
f = g
let a, b be Element of OAS; :: thesis: for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds
f = g
let f, g be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b implies f = g )
assume that
A1: ( f is dilatation & g is dilatation ) and
A2: ( f . a = g . a & f . b = g . b ) ; :: thesis: ( a = b or f = g )
assume A3: a <> b ; :: thesis: f = g
A4: ((g " ) * f) . a = (g " ) . (g . a) by A2, FUNCT_2:21
.= a by Th4 ;
A5: ((g " ) * f) . b = (g " ) . (g . b) by A2, FUNCT_2:21
.= b by Th4 ;
g " is dilatation by A1, Th56;
then A6: (g " ) * f = id the carrier of OAS by A1, A3, A4, A5, Th57, Th64;

now

let x be Element of OAS; :: thesis: g . x = f . x
(g " ) . (f . x) = ((g " ) * f) . x by FUNCT_2:21;
then (g " ) . (f . x) = x by A6, FUNCT_1:35;
hence g . x = f . x by Th4; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum