let AFS be AffinSpace; :: thesis: for a, x being Element of AFS
for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds
f . x = g . x
let a, x be Element of AFS; :: thesis: for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds
f . x = g . x
let f, g be Permutation of the carrier of AFS; :: thesis: ( f is translation & g is translation & f . a = g . a & not LIN a,f . a,x 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 LIN a,f . a,x ; :: thesis: f . x = g . x
set b = f . a;
set y = f . x;
set z = g . x;
g is dilatation by A2, Def11;
then A5: ( a,x // f . a,g . x & a,f . a // x,g . x ) by A2, A3, Th85, Th100;
A6: f is dilatation by A1, Def11;
then A7: a,x // f . a,f . x by Th85;
a,f . a // x,f . x by A1, A6, Th100;
hence f . x = g . x by A4, A7, A5, Th97; :: thesis: verum