let AFP be AffinPlane; for a, b being Element of AFP
for K being Subset of AFP 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 AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
let a, b be Element of AFP; for K being Subset of AFP 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 AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
let K be Subset of AFP; ( 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 AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) )
defpred S1[ Element of AFP, Element of AFP] means ( ( $1 in K & $1 = $2 ) or ( not $1 in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,$1 & p,b // p9,$2 & $1,$2 // K ) ) );
assume that
A1:
a,b // K
and
A2:
not a in K
and
A3:
AFP is Moufangian
; ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
A4:
for x, y, s being Element of AFP st S1[x,y] & S1[x,s] holds
y = s
by A1, A2, A3, Lm22;
A5:
for y being Element of AFP ex x being Element of AFP st S1[x,y]
by A1, A2, Lm20;
A6:
for x being Element of AFP ex y being Element of AFP st S1[x,y]
by A1, A2, Lm19;
A7:
for x, y, r being Element of AFP st S1[x,y] & S1[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 AFP holds
( f . x = y iff S1[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 AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
; verum