let k be Nat; :: thesis: for X being non empty set st 1 < k & card X = k + 1 holds

for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

let X be non empty set ; :: thesis: ( 1 < k & card X = k + 1 implies for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )

assume that

A1: 1 < k and

A2: k + 1 = card X ; :: thesis: for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

deffunc H_{1}( object ) -> Element of bool X = X \ {$1};

consider c being Function such that

A3: dom c = X and

A4: for x being object st x in X holds

c . x = H_{1}(x)
from FUNCT_1:sch 3();

A5: X is finite by A2;

A6: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, A2, Def1;

A7: rng c c= the Points of (G_ (k,X))

assume F is automorphism ; :: thesis: ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

then A12: the point-map of F is bijective ;

reconsider c = c as Function of X, the Points of (G_ (k,X)) by A3, A7, FUNCT_2:2;

deffunc H_{2}( Element of X) -> set = union (X \ (F . (c . $1)));

consider f being Function such that

A13: dom f = X and

A14: for x being Element of X holds f . x = H_{2}(x)
from FUNCT_1:sch 4();

rng f c= X

A20: dom the point-map of F = the Points of (G_ (k,X)) by FUNCT_2:52;

A21: f is one-to-one

for y being object st y in X holds

ex x being object st

( x in X & y = f . x )

then f is onto by FUNCT_2:def 3;

then reconsider f = f as Permutation of X by A21;

A40: dom the line-map of F = the Lines of (G_ (k,X)) by FUNCT_2:52;

A41: for x being object st x in dom the point-map of F holds

the point-map of F . x = the point-map of (incprojmap (k,f)) . x

then A52: the point-map of F = the point-map of (incprojmap (k,f)) by A20, A41;

A53: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A2, Def1;

A54: for x being object st x in dom the line-map of F holds

the line-map of F . x = the line-map of (incprojmap (k,f)) . x

then IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,f) by A40, A52, A54, FUNCT_1:def 11;

hence ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ; :: thesis: verum

for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

let X be non empty set ; :: thesis: ( 1 < k & card X = k + 1 implies for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )

assume that

A1: 1 < k and

A2: k + 1 = card X ; :: thesis: for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds

ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

deffunc H

consider c being Function such that

A3: dom c = X and

A4: for x being object st x in X holds

c . x = H

A5: X is finite by A2;

A6: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, A2, Def1;

A7: rng c c= the Points of (G_ (k,X))

proof

let F be IncProjMap over G_ (k,X), G_ (k,X); :: thesis: ( F is automorphism implies ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in the Points of (G_ (k,X)) )

assume y in rng c ; :: thesis: y in the Points of (G_ (k,X))

then consider x being object such that

A8: x in dom c and

A9: y = c . x by FUNCT_1:def 3;

A10: card {x} = 1 by CARD_1:30;

{x} c= X by A3, A8, ZFMISC_1:31;

then A11: card (X \ {x}) = (k + 1) - 1 by A2, A5, A10, CARD_2:44;

y = X \ {x} by A3, A4, A8, A9;

hence y in the Points of (G_ (k,X)) by A6, A11; :: thesis: verum

end;assume y in rng c ; :: thesis: y in the Points of (G_ (k,X))

then consider x being object such that

A8: x in dom c and

A9: y = c . x by FUNCT_1:def 3;

A10: card {x} = 1 by CARD_1:30;

{x} c= X by A3, A8, ZFMISC_1:31;

then A11: card (X \ {x}) = (k + 1) - 1 by A2, A5, A10, CARD_2:44;

y = X \ {x} by A3, A4, A8, A9;

hence y in the Points of (G_ (k,X)) by A6, A11; :: thesis: verum

assume F is automorphism ; :: thesis: ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s)

then A12: the point-map of F is bijective ;

reconsider c = c as Function of X, the Points of (G_ (k,X)) by A3, A7, FUNCT_2:2;

deffunc H

consider f being Function such that

A13: dom f = X and

A14: for x being Element of X holds f . x = H

rng f c= X

proof

then reconsider f = f as Function of X,X by A13, FUNCT_2:2;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng f or b in X )

assume b in rng f ; :: thesis: b in X

then consider a being object such that

A15: a in X and

A16: b = f . a by A13, FUNCT_1:def 3;

reconsider a = a as Element of X by A15;

A17: b = union (X \ (F . (c . a))) by A14, A16;

consider A being POINT of (G_ (k,X)) such that

A18: A = F . (c . a) ;

A in the Points of (G_ (k,X)) ;

then ex A1 being Subset of X st

( A1 = A & card A1 = k ) by A6;

then card (X \ A) = (k + 1) - k by A2, A5, CARD_2:44;

then consider x being object such that

A19: X \ A = {x} by CARD_2:42;

x in X by A19, ZFMISC_1:31;

hence b in X by A17, A18, A19, ZFMISC_1:25; :: thesis: verum

end;assume b in rng f ; :: thesis: b in X

then consider a being object such that

A15: a in X and

A16: b = f . a by A13, FUNCT_1:def 3;

reconsider a = a as Element of X by A15;

A17: b = union (X \ (F . (c . a))) by A14, A16;

consider A being POINT of (G_ (k,X)) such that

A18: A = F . (c . a) ;

A in the Points of (G_ (k,X)) ;

then ex A1 being Subset of X st

( A1 = A & card A1 = k ) by A6;

then card (X \ A) = (k + 1) - k by A2, A5, CARD_2:44;

then consider x being object such that

A19: X \ A = {x} by CARD_2:42;

x in X by A19, ZFMISC_1:31;

hence b in X by A17, A18, A19, ZFMISC_1:25; :: thesis: verum

A20: dom the point-map of F = the Points of (G_ (k,X)) by FUNCT_2:52;

A21: f is one-to-one

proof

A32:
rng the point-map of F = the Points of (G_ (k,X))
by A12, FUNCT_2:def 3;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A22: ( x1 in dom f & x2 in dom f ) and

A23: f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as Element of X by A22;

consider A1 being POINT of (G_ (k,X)) such that

A24: A1 = F . (c . x1) ;

consider A2 being POINT of (G_ (k,X)) such that

A25: A2 = F . (c . x2) ;

A2 in the Points of (G_ (k,X)) ;

then A26: ex A12 being Subset of X st

( A12 = A2 & card A12 = k ) by A6;

then card (X \ A2) = (k + 1) - k by A2, A5, CARD_2:44;

then consider y2 being object such that

A27: X \ A2 = {y2} by CARD_2:42;

A1 in the Points of (G_ (k,X)) ;

then A28: ex A11 being Subset of X st

( A11 = A1 & card A11 = k ) by A6;

then card (X \ A1) = (k + 1) - k by A2, A5, CARD_2:44;

then consider y1 being object such that

A29: X \ A1 = {y1} by CARD_2:42;

f . x2 = union (X \ (F . (c . x2))) by A14;

then A30: f . x2 = y2 by A25, A27, ZFMISC_1:25;

f . x1 = union (X \ (F . (c . x1))) by A14;

then f . x1 = y1 by A24, A29, ZFMISC_1:25;

then A1 = A2 by A23, A28, A26, A29, A27, A30, Th5;

then A31: c . x1 = c . x2 by A12, A20, A24, A25, FUNCT_1:def 4;

( c . x1 = X \ {x1} & c . x2 = X \ {x2} ) by A4;

then {x1} = {x2} by A31, Th5;

hence x1 = x2 by ZFMISC_1:3; :: thesis: verum

end;assume that

A22: ( x1 in dom f & x2 in dom f ) and

A23: f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as Element of X by A22;

consider A1 being POINT of (G_ (k,X)) such that

A24: A1 = F . (c . x1) ;

consider A2 being POINT of (G_ (k,X)) such that

A25: A2 = F . (c . x2) ;

A2 in the Points of (G_ (k,X)) ;

then A26: ex A12 being Subset of X st

( A12 = A2 & card A12 = k ) by A6;

then card (X \ A2) = (k + 1) - k by A2, A5, CARD_2:44;

then consider y2 being object such that

A27: X \ A2 = {y2} by CARD_2:42;

A1 in the Points of (G_ (k,X)) ;

then A28: ex A11 being Subset of X st

( A11 = A1 & card A11 = k ) by A6;

then card (X \ A1) = (k + 1) - k by A2, A5, CARD_2:44;

then consider y1 being object such that

A29: X \ A1 = {y1} by CARD_2:42;

f . x2 = union (X \ (F . (c . x2))) by A14;

then A30: f . x2 = y2 by A25, A27, ZFMISC_1:25;

f . x1 = union (X \ (F . (c . x1))) by A14;

then f . x1 = y1 by A24, A29, ZFMISC_1:25;

then A1 = A2 by A23, A28, A26, A29, A27, A30, Th5;

then A31: c . x1 = c . x2 by A12, A20, A24, A25, FUNCT_1:def 4;

( c . x1 = X \ {x1} & c . x2 = X \ {x2} ) by A4;

then {x1} = {x2} by A31, Th5;

hence x1 = x2 by ZFMISC_1:3; :: thesis: verum

for y being object st y in X holds

ex x being object st

( x in X & y = f . x )

proof

then A39:
rng f = X
by FUNCT_2:10;
let y be object ; :: thesis: ( y in X implies ex x being object st

( x in X & y = f . x ) )

assume y in X ; :: thesis: ex x being object st

( x in X & y = f . x )

then A33: {y} c= X by ZFMISC_1:31;

card {y} = 1 by CARD_1:30;

then card (X \ {y}) = (k + 1) - 1 by A2, A5, A33, CARD_2:44;

then X \ {y} in rng the point-map of F by A6, A32;

then consider a being object such that

A34: a in dom the point-map of F and

A35: X \ {y} = the point-map of F . a by FUNCT_1:def 3;

reconsider a = a as set by TARSKI:1;

a in the Points of (G_ (k,X)) by A34;

then A36: ex A1 being Subset of X st

( A1 = a & card A1 = k ) by A6;

then card (X \ a) = (k + 1) - k by A2, A5, CARD_2:44;

then consider x being object such that

A37: X \ a = {x} by CARD_2:42;

reconsider x = x as Element of X by A37, ZFMISC_1:31;

a /\ X = X \ {x} by A37, XBOOLE_1:48;

then A38: X \ {x} = a by A36, XBOOLE_1:28;

c . x = X \ {x} by A4;

then X /\ {y} = X \ (F . (c . x)) by A35, A38, XBOOLE_1:48;

then {y} = X \ (F . (c . x)) by A33, XBOOLE_1:28;

then y = union (X \ (F . (c . x))) by ZFMISC_1:25;

then y = f . x by A14;

hence ex x being object st

( x in X & y = f . x ) ; :: thesis: verum

end;( x in X & y = f . x ) )

assume y in X ; :: thesis: ex x being object st

( x in X & y = f . x )

then A33: {y} c= X by ZFMISC_1:31;

card {y} = 1 by CARD_1:30;

then card (X \ {y}) = (k + 1) - 1 by A2, A5, A33, CARD_2:44;

then X \ {y} in rng the point-map of F by A6, A32;

then consider a being object such that

A34: a in dom the point-map of F and

A35: X \ {y} = the point-map of F . a by FUNCT_1:def 3;

reconsider a = a as set by TARSKI:1;

a in the Points of (G_ (k,X)) by A34;

then A36: ex A1 being Subset of X st

( A1 = a & card A1 = k ) by A6;

then card (X \ a) = (k + 1) - k by A2, A5, CARD_2:44;

then consider x being object such that

A37: X \ a = {x} by CARD_2:42;

reconsider x = x as Element of X by A37, ZFMISC_1:31;

a /\ X = X \ {x} by A37, XBOOLE_1:48;

then A38: X \ {x} = a by A36, XBOOLE_1:28;

c . x = X \ {x} by A4;

then X /\ {y} = X \ (F . (c . x)) by A35, A38, XBOOLE_1:48;

then {y} = X \ (F . (c . x)) by A33, XBOOLE_1:28;

then y = union (X \ (F . (c . x))) by ZFMISC_1:25;

then y = f . x by A14;

hence ex x being object st

( x in X & y = f . x ) ; :: thesis: verum

then f is onto by FUNCT_2:def 3;

then reconsider f = f as Permutation of X by A21;

A40: dom the line-map of F = the Lines of (G_ (k,X)) by FUNCT_2:52;

A41: for x being object st x in dom the point-map of F holds

the point-map of F . x = the point-map of (incprojmap (k,f)) . x

proof

dom the point-map of (incprojmap (k,f)) = the Points of (G_ (k,X))
by FUNCT_2:52;
let x be object ; :: thesis: ( x in dom the point-map of F implies the point-map of F . x = the point-map of (incprojmap (k,f)) . x )

assume A42: x in dom the point-map of F ; :: thesis: the point-map of F . x = the point-map of (incprojmap (k,f)) . x

then consider A being POINT of (G_ (k,X)) such that

A43: x = A ;

F . A in the Points of (G_ (k,X)) ;

then A44: ex B being Subset of X st

( B = F . A & card B = k ) by A6;

then card (X \ (F . A)) = (k + 1) - k by A2, A5, CARD_2:44;

then A45: ex x2 being object st X \ (F . A) = {x2} by CARD_2:42;

( X \ (X \ (F . A)) = (F . A) /\ X & (F . A) /\ X = F . A ) by A44, XBOOLE_1:28, XBOOLE_1:48;

then A46: F . A = X \ {(union (X \ (F . A)))} by A45, ZFMISC_1:25;

A47: f .: X = X by A39, RELSET_1:22;

A48: ex A1 being Subset of X st

( x = A1 & card A1 = k ) by A6, A20, A42;

then A49: ( X \ (X \ A) = A /\ X & A /\ X = A ) by A43, XBOOLE_1:28, XBOOLE_1:48;

card (X \ A) = (k + 1) - k by A2, A5, A43, A48, CARD_2:44;

then consider x1 being object such that

A50: X \ A = {x1} by CARD_2:42;

reconsider x1 = x1 as Element of X by A50, ZFMISC_1:31;

A51: ( c . x1 = X \ {x1} & Im (f,x1) = {(f . x1)} ) by A4, A13, FUNCT_1:59;

(incprojmap (k,f)) . A = f .: A by A1, A2, Def14;

then (incprojmap (k,f)) . A = (f .: X) \ (f .: {x1}) by A50, A49, FUNCT_1:64;

hence the point-map of F . x = the point-map of (incprojmap (k,f)) . x by A14, A43, A50, A46, A49, A51, A47; :: thesis: verum

end;assume A42: x in dom the point-map of F ; :: thesis: the point-map of F . x = the point-map of (incprojmap (k,f)) . x

then consider A being POINT of (G_ (k,X)) such that

A43: x = A ;

F . A in the Points of (G_ (k,X)) ;

then A44: ex B being Subset of X st

( B = F . A & card B = k ) by A6;

then card (X \ (F . A)) = (k + 1) - k by A2, A5, CARD_2:44;

then A45: ex x2 being object st X \ (F . A) = {x2} by CARD_2:42;

( X \ (X \ (F . A)) = (F . A) /\ X & (F . A) /\ X = F . A ) by A44, XBOOLE_1:28, XBOOLE_1:48;

then A46: F . A = X \ {(union (X \ (F . A)))} by A45, ZFMISC_1:25;

A47: f .: X = X by A39, RELSET_1:22;

A48: ex A1 being Subset of X st

( x = A1 & card A1 = k ) by A6, A20, A42;

then A49: ( X \ (X \ A) = A /\ X & A /\ X = A ) by A43, XBOOLE_1:28, XBOOLE_1:48;

card (X \ A) = (k + 1) - k by A2, A5, A43, A48, CARD_2:44;

then consider x1 being object such that

A50: X \ A = {x1} by CARD_2:42;

reconsider x1 = x1 as Element of X by A50, ZFMISC_1:31;

A51: ( c . x1 = X \ {x1} & Im (f,x1) = {(f . x1)} ) by A4, A13, FUNCT_1:59;

(incprojmap (k,f)) . A = f .: A by A1, A2, Def14;

then (incprojmap (k,f)) . A = (f .: X) \ (f .: {x1}) by A50, A49, FUNCT_1:64;

hence the point-map of F . x = the point-map of (incprojmap (k,f)) . x by A14, A43, A50, A46, A49, A51, A47; :: thesis: verum

then A52: the point-map of F = the point-map of (incprojmap (k,f)) by A20, A41;

A53: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A2, Def1;

A54: for x being object st x in dom the line-map of F holds

the line-map of F . x = the line-map of (incprojmap (k,f)) . x

proof

dom the line-map of (incprojmap (k,f)) = the Lines of (G_ (k,X))
by FUNCT_2:52;
let x be object ; :: thesis: ( x in dom the line-map of F implies the line-map of F . x = the line-map of (incprojmap (k,f)) . x )

assume A55: x in dom the line-map of F ; :: thesis: the line-map of F . x = the line-map of (incprojmap (k,f)) . x

then consider A being LINE of (G_ (k,X)) such that

A56: x = A ;

F . A in the Lines of (G_ (k,X)) ;

then ex y being Subset of X st

( y = F . A & card y = k + 1 ) by A53;

then A57: F . A = X by A2, A5, CARD_2:102;

ex A11 being Subset of X st

( x = A11 & card A11 = k + 1 ) by A53, A40, A55;

then A58: x = X by A2, A5, CARD_2:102;

reconsider xx = x as set by TARSKI:1;

(incprojmap (k,f)) . A = f .: xx by A1, A2, A56, Def14;

hence the line-map of F . x = the line-map of (incprojmap (k,f)) . x by A39, A56, A58, A57, RELSET_1:22; :: thesis: verum

end;assume A55: x in dom the line-map of F ; :: thesis: the line-map of F . x = the line-map of (incprojmap (k,f)) . x

then consider A being LINE of (G_ (k,X)) such that

A56: x = A ;

F . A in the Lines of (G_ (k,X)) ;

then ex y being Subset of X st

( y = F . A & card y = k + 1 ) by A53;

then A57: F . A = X by A2, A5, CARD_2:102;

ex A11 being Subset of X st

( x = A11 & card A11 = k + 1 ) by A53, A40, A55;

then A58: x = X by A2, A5, CARD_2:102;

reconsider xx = x as set by TARSKI:1;

(incprojmap (k,f)) . A = f .: xx by A1, A2, A56, Def14;

hence the line-map of F . x = the line-map of (incprojmap (k,f)) . x by A39, A56, A58, A57, RELSET_1:22; :: thesis: verum

then IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,f) by A40, A52, A54, FUNCT_1:def 11;

hence ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ; :: thesis: verum