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 & not p in K ) ; :: thesis: f = id the carrier of AFP
( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) ) by A1, Def1;
hence f = id the carrier of AFP by A2, TRANSGEO:117; :: thesis: verum