let AFS be AffinSpace; :: thesis: for a, b, x being Element of AFS

for f being Permutation of the carrier of AFS 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 AFS; :: thesis: for f being Permutation of the carrier of AFS 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 AFS; :: 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 and

A3: f . b = b and

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

a,x // a,f . x by A1, A2, Th68;

then LIN a,x,f . x by AFF_1:def 1;

then A5: LIN x,f . x,a by AFF_1:6;

b,x // b,f . x by A1, A3, Th68;

then LIN b,x,f . x by AFF_1:def 1;

then A6: ( LIN x,f . x,x & LIN x,f . x,b ) by AFF_1:6, AFF_1:7;

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

hence contradiction by A4, A5, A6, AFF_1:8; :: thesis: verum

for f being Permutation of the carrier of AFS 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 AFS; :: thesis: for f being Permutation of the carrier of AFS 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 AFS; :: 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 and

A3: f . b = b and

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

a,x // a,f . x by A1, A2, Th68;

then LIN a,x,f . x by AFF_1:def 1;

then A5: LIN x,f . x,a by AFF_1:6;

b,x // b,f . x by A1, A3, Th68;

then LIN b,x,f . x by AFF_1:def 1;

then A6: ( LIN x,f . x,x & LIN x,f . x,b ) by AFF_1:6, AFF_1:7;

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

hence contradiction by A4, A5, A6, AFF_1:8; :: thesis: verum