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 LIN a,b,x 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 LIN a,b,x holds
f . x = x
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . a = a & f . b = b & not LIN a,b,x implies f . x = x )
assume that
A1: f is dilatation and
A2: ( f . a = a & f . b = b ) and
A3: not LIN a,b,x ; :: thesis: f . x = x
assume A4: f . x <> x ; :: thesis: contradiction
a,x '||' a,f . x by A1, A2, Th51;
then LIN a,x,f . x by DIRAF:def 5;
then A5: LIN x,f . x,a by DIRAF:36;
b,x '||' b,f . x by A1, A2, Th51;
then LIN b,x,f . x by DIRAF:def 5;
then ( LIN x,f . x,x & LIN x,f . x,b ) by DIRAF:36, DIRAF:37;
hence contradiction by A3, A4, A5, DIRAF:38; :: thesis: verum