let OAS be OAffinSpace; :: thesis: for a, b, x being Element of OAS

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

f . x = x

let a, b, x be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & not a,b,x are_collinear holds

f . x = x

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

assume that

A1: f is dilatation and

A2: f . a = a and

A3: f . b = b and

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

a,x '||' a,f . x by A1, A2, Th34;

then a,x,f . x are_collinear by DIRAF:def 5;

then A5: x,f . x,a are_collinear by DIRAF:30;

b,x '||' b,f . x by A1, A3, Th34;

then b,x,f . x are_collinear by DIRAF:def 5;

then A6: ( x,f . x,x are_collinear & x,f . x,b are_collinear ) by DIRAF:30, DIRAF:31;

assume f . x <> x ; :: thesis: contradiction

hence contradiction by A4, A5, A6, DIRAF:32; :: thesis: verum

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

f . x = x

let a, b, x be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & not a,b,x are_collinear holds

f . x = x

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

assume that

A1: f is dilatation and

A2: f . a = a and

A3: f . b = b and

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

a,x '||' a,f . x by A1, A2, Th34;

then a,x,f . x are_collinear by DIRAF:def 5;

then A5: x,f . x,a are_collinear by DIRAF:30;

b,x '||' b,f . x by A1, A3, Th34;

then b,x,f . x are_collinear by DIRAF:def 5;

then A6: ( x,f . x,x are_collinear & x,f . x,b are_collinear ) by DIRAF:30, DIRAF:31;

assume f . x <> x ; :: thesis: contradiction

hence contradiction by A4, A5, A6, DIRAF:32; :: thesis: verum