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;

hence f = g by A5; :: thesis: verum

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 )

( f . a = a implies f = g )
by A1, A2, A3;assume A6:
a <> f . a
; :: thesis: f = g

for x being Element of OAS holds f . x = g . x

end;for x being Element of OAS holds f . x = g . x

proof

hence
f = g
by FUNCT_2:63; :: thesis: verum
let x be Element of OAS; :: thesis: f . x = g . x

end;now :: thesis: ( a,f . a,x are_collinear implies f . x = g . x )

hence
f . x = g . x
by A1, A2, A3, Th54; :: thesis: verumassume A7:
a,f . a,x are_collinear
; :: thesis: f . x = g . x

end;now :: thesis: ( x <> a implies f . x = g . x )

hence
f . x = g . x
by A3; :: thesis: verumA8:
f <> id the carrier of OAS
by A6;

then A9: f . x <> x by A1;

assume x <> a ; :: thesis: f . x = g . x

consider p being Element of OAS such that

A10: not a,f . a,p are_collinear by A6, DIRAF:37;

A11: f . p <> p by A1, A8;

A12: not p,f . p,x are_collinear

hence f . x = g . x by A1, A2, A12, Th54; :: thesis: verum

end;then A9: f . x <> x by A1;

assume x <> a ; :: thesis: f . x = g . x

consider p being Element of OAS such that

A10: not a,f . a,p are_collinear by A6, DIRAF:37;

A11: f . p <> p by A1, A8;

A12: not p,f . p,x are_collinear

proof

f . p = g . p
by A1, A2, A3, A10, Th54;
A13:
a,f . a,f . x are_collinear
by A4, A7, Th47;

a,f . a,a are_collinear by DIRAF:31;

then A14: x,f . x,a are_collinear by A6, A7, A13, DIRAF:32;

A15: p,f . p,p are_collinear by DIRAF:31;

a,f . a,f . a are_collinear by DIRAF:31;

then A16: x,f . x,f . a are_collinear by A6, A7, A13, DIRAF:32;

assume A17: p,f . p,x are_collinear ; :: thesis: contradiction

then p,f . p,f . x are_collinear by A4, Th47;

then x,f . x,p are_collinear by A11, A17, A15, DIRAF:32;

hence contradiction by A10, A9, A14, A16, DIRAF:32; :: thesis: verum

end;a,f . a,a are_collinear by DIRAF:31;

then A14: x,f . x,a are_collinear by A6, A7, A13, DIRAF:32;

A15: p,f . p,p are_collinear by DIRAF:31;

a,f . a,f . a are_collinear by DIRAF:31;

then A16: x,f . x,f . a are_collinear by A6, A7, A13, DIRAF:32;

assume A17: p,f . p,x are_collinear ; :: thesis: contradiction

then p,f . p,f . x are_collinear by A4, Th47;

then x,f . x,p are_collinear by A11, A17, A15, DIRAF:32;

hence contradiction by A10, A9, A14, A16, DIRAF:32; :: thesis: verum

hence f . x = g . x by A1, A2, A12, Th54; :: thesis: verum

hence f = g by A5; :: thesis: verum