let OAS be OAffinSpace; :: thesis: for a, x 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 & not a,f . a,x are_collinear holds

f . x = g . x

let a, x 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 & not a,f . a,x are_collinear holds

f . x = g . x

let f, g be Permutation of the carrier of OAS; :: thesis: ( f is translation & g is translation & f . a = g . a & not a,f . a,x are_collinear implies f . x = g . x )

assume that

A1: f is translation and

A2: g is translation and

A3: f . a = g . a and

A4: not a,f . a,x are_collinear ; :: thesis: f . x = g . x

set b = f . a;

set y = f . x;

set z = g . x;

A5: ( a,x '||' f . a,g . x & a,f . a '||' x,g . x ) by A2, A3, Th34, Th53;

f is dilatation by A1;

then A6: a,x '||' f . a,f . x by Th34;

a,f . a '||' x,f . x by A1, Th53;

hence f . x = g . x by A4, A6, A5, PASCH:5; :: thesis: verum

for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a & not a,f . a,x are_collinear holds

f . x = g . x

let a, x 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 & not a,f . a,x are_collinear holds

f . x = g . x

let f, g be Permutation of the carrier of OAS; :: thesis: ( f is translation & g is translation & f . a = g . a & not a,f . a,x are_collinear implies f . x = g . x )

assume that

A1: f is translation and

A2: g is translation and

A3: f . a = g . a and

A4: not a,f . a,x are_collinear ; :: thesis: f . x = g . x

set b = f . a;

set y = f . x;

set z = g . x;

A5: ( a,x '||' f . a,g . x & a,f . a '||' x,g . x ) by A2, A3, Th34, Th53;

f is dilatation by A1;

then A6: a,x '||' f . a,f . x by Th34;

a,f . a '||' x,f . x by A1, Th53;

hence f . x = g . x by A4, A6, A5, PASCH:5; :: thesis: verum