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 LIN a,f . a,x 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 LIN a,f . a,x 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 LIN a,f . a,x implies f . x = g . x )
assume that
A1: ( f is translation & g is translation ) and
A2: f . a = g . a and
A3: not LIN a,f . a,x ; :: thesis: f . x = g . x
A4: ( f is dilatation & g is dilatation ) by A1, Def9;
set b = f . a;
set y = f . x;
set z = g . x;
A5: ( a,x '||' f . a,f . x & a,f . a '||' x,f . x ) by A1, A4, Th51, Th67;
( a,x '||' f . a,g . x & a,f . a '||' x,g . x ) by A1, A2, A4, Th51, Th67;
hence f . x = g . x by A3, A5, PASCH:12; :: thesis: verum