let AFP be AffinPlane; :: thesis: for K being Subset of AFP
for p being Element of AFP
for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP

let K be Subset of AFP; :: thesis: for p being Element of AFP
for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP

let p be Element of AFP; :: thesis: for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP

let f be Permutation of the carrier of AFP; :: thesis: ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p implies f = id the carrier of AFP )

assume that
A1: f is collineation and
A2: K is being_line and
A3: for x being Element of AFP st x in K holds
f . x = x and
A4: not p in K and
A5: f . p = p ; :: thesis: f = id the carrier of AFP
A6: for x being Element of AFP holds f . x = x
proof
let x be Element of AFP; :: thesis: f . x = x
now :: thesis: ( not x in K implies f . x = x )
assume not x in K ; :: thesis: f . x = x
consider a, b being Element of AFP such that
A7: a in K and
A8: b in K and
A9: a <> b by ;
set A = Line (p,a);
A10: p in Line (p,a) by AFF_1:15;
f .: (Line (p,a)) = Line ((f . p),(f . a)) by ;
then A11: f .: (Line (p,a)) = Line (p,a) by A3, A5, A7;
Line (p,a) is being_line by ;
then consider C being Subset of AFP such that
A12: x in C and
A13: Line (p,a) // C by AFF_1:49;
A14: C is being_line by ;
f .: (Line (p,a)) // f .: C by ;
then A15: f .: C // C by ;
A16: a in Line (p,a) by AFF_1:15;
not C // K
proof
assume C // K ; :: thesis: contradiction
then Line (p,a) // K by ;
hence contradiction by A4, A7, A10, A16, AFF_1:45; :: thesis: verum
end;
then consider c being Element of AFP such that
A17: c in C and
A18: c in K by ;
f . c = c by ;
then c in f .: C by ;
then A19: f .: C = C by ;
set M = Line (p,b);
A20: b in Line (p,b) by AFF_1:15;
f .: (Line (p,b)) = Line ((f . p),(f . b)) by ;
then A21: f .: (Line (p,b)) = Line (p,b) by A3, A5, A8;
Line (p,b) is being_line by ;
then consider D being Subset of AFP such that
A22: x in D and
A23: Line (p,b) // D by AFF_1:49;
A24: D is being_line by ;
f .: (Line (p,b)) // f .: D by ;
then A25: f .: D // D by ;
A26: p in Line (p,b) by AFF_1:15;
not D // K
proof
assume D // K ; :: thesis: contradiction
then Line (p,b) // K by ;
hence contradiction by A4, A8, A26, A20, AFF_1:45; :: thesis: verum
end;
then consider d being Element of AFP such that
A27: d in D and
A28: d in K by ;
f . d = d by ;
then d in f .: D by ;
then A29: f .: D = D by ;
A30: Line (p,a) is being_line by ;
x = f . x
proof
assume A31: x <> f . x ; :: thesis: contradiction
( f . x in C & f . x in D ) by A12, A22, A19, A29, Th90;
then C = D by ;
then Line (p,a) // Line (p,b) by ;
then Line (p,a) = Line (p,b) by ;
hence contradiction by A2, A4, A7, A8, A9, A30, A10, A16, A20, AFF_1:18; :: thesis: verum
end;
hence f . x = x ; :: thesis: verum
end;
hence f . x = x by A3; :: thesis: verum
end;
for x being Element of AFP holds f . x = (id the carrier of AFP) . x by A6;
hence f = id the carrier of AFP by FUNCT_2:63; :: thesis: verum