let AFP be AffinPlane; :: thesis: for a, b being Element of
for K being Subset of st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) )
let a, b be Element of ; :: thesis: for K being Subset of st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) )
let K be Subset of ; :: thesis: ( a,b // K & not a in K & AFP is Moufangian implies ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) )
defpred S₁[ Element of , Element of ] means ( ( $1 in K & $1 = $2 ) or ( not $1 in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',$1 & p,b // p',$2 & $1,$2 // K ) ) );
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian ; :: thesis: ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) )
A4: for x, y, s being Element of st S₁[x,y] & S₁[x,s] holds
y = s by A1, A2, A3, Lm22;
A5: for y being Element of ex x being Element of st S₁[x,y] by A1, A2, Lm20;
A6: for x being Element of ex y being Element of st S₁[x,y] by A1, A2, Lm19;
A7: for x, y, r being Element of st S₁[x,y] & S₁[r,y] holds
x = r by A1, A2, A3, Lm23;
ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff S₁[x,y] ) from TRANSGEO:sch 1(A6, A5, A7, A4);
hence ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ; :: thesis: verum