let AFP be AffinPlane; :: thesis: for p being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
let p be Element of AFP; :: thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
let K be Subset of AFP; :: thesis: for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
let f be Permutation of the carrier of AFP; :: thesis: ( f is_Sc K & f . p = p & not p in K implies f = id the carrier of AFP )
assume that
A1: f is_Sc K and
A2: f . p = p and
A3: not p in K ; :: thesis: f = id the carrier of AFP
A4: K is being_line by A1, Def1;
A5: for x being Element of AFP st x in K holds
f . x = x by A1, Def1;
f is collineation by A1, Def1;
hence f = id the carrier of AFP by A2, A3, A4, A5, TRANSGEO:93; :: thesis: verum