let AFS be AffinSpace; :: thesis: for a 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 holds

f = g

let a 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 holds

f = g

let f, g be Permutation of the carrier of AFS; :: thesis: ( f is translation & g is translation & f . a = g . a implies f = g )

assume that

A1: f is translation and

A2: g is translation and

A3: f . a = g . a ; :: thesis: f = g

set b = f . a;

A4: f is dilatation by A1;

hence f = g by A5; :: thesis: verum

for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds

f = g

let a 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 holds

f = g

let f, g be Permutation of the carrier of AFS; :: thesis: ( f is translation & g is translation & f . a = g . a implies f = g )

assume that

A1: f is translation and

A2: g is translation and

A3: f . a = g . a ; :: thesis: f = g

set b = f . a;

A4: f is dilatation by A1;

A5: now :: thesis: ( a <> f . a implies f = g )

( f . a = a implies f = g )
by A1, A2, A3;assume A6:
a <> f . a
; :: thesis: f = g

for x being Element of AFS holds f . x = g . x

end;for x being Element of AFS holds f . x = g . x

proof

hence
f = g
by FUNCT_2:63; :: thesis: verum
let x be Element of AFS; :: thesis: f . x = g . x

end;now :: thesis: ( LIN a,f . a,x implies f . x = g . x )

hence
f . x = g . x
by A1, A2, A3, Th83; :: thesis: verumassume A7:
LIN a,f . a,x
; :: thesis: f . x = g . x

end;now :: thesis: ( x <> a implies f . x = g . x )

hence
f . x = g . x
by A3; :: thesis: verumA8:
f <> id the carrier of AFS
by A6;

then A9: f . x <> x by A1;

assume x <> a ; :: thesis: f . x = g . x

consider p being Element of AFS such that

A10: not LIN a,f . a,p by A6, AFF_1:13;

A11: f . p <> p by A1, A8;

A12: not LIN p,f . p,x

hence f . x = g . x by A1, A2, A12, Th83; :: thesis: verum

end;then A9: f . x <> x by A1;

assume x <> a ; :: thesis: f . x = g . x

consider p being Element of AFS such that

A10: not LIN a,f . a,p by A6, AFF_1:13;

A11: f . p <> p by A1, A8;

A12: not LIN p,f . p,x

proof

f . p = g . p
by A1, A2, A3, A10, Th83;
A13:
LIN a,f . a,f . x
by A4, A7, Th74;

LIN a,f . a,a by AFF_1:7;

then A14: LIN x,f . x,a by A6, A7, A13, AFF_1:8;

A15: LIN p,f . p,p by AFF_1:7;

LIN a,f . a,f . a by AFF_1:7;

then A16: LIN x,f . x,f . a by A6, A7, A13, AFF_1:8;

assume A17: LIN p,f . p,x ; :: thesis: contradiction

then LIN p,f . p,f . x by A4, Th74;

then LIN x,f . x,p by A11, A17, A15, AFF_1:8;

hence contradiction by A10, A9, A14, A16, AFF_1:8; :: thesis: verum

end;LIN a,f . a,a by AFF_1:7;

then A14: LIN x,f . x,a by A6, A7, A13, AFF_1:8;

A15: LIN p,f . p,p by AFF_1:7;

LIN a,f . a,f . a by AFF_1:7;

then A16: LIN x,f . x,f . a by A6, A7, A13, AFF_1:8;

assume A17: LIN p,f . p,x ; :: thesis: contradiction

then LIN p,f . p,f . x by A4, Th74;

then LIN x,f . x,p by A11, A17, A15, AFF_1:8;

hence contradiction by A10, A9, A14, A16, AFF_1:8; :: thesis: verum

hence f . x = g . x by A1, A2, A12, Th83; :: thesis: verum

hence f = g by A5; :: thesis: verum