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 H1( 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 = H1(x) from 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 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 ;
then A11: card (X \ {x}) = (k + 1) - 1 by ;
y = X \ {x} by A3, A4, A8, A9;
hence y in the Points of (G_ (k,X)) by ; :: thesis: verum
end;
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) )
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 ;
deffunc H2( 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 = H2(x) from rng f c= X
proof
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 ;
reconsider a = a as Element of X by A15;
A17: b = union (X \ (F . (c . a))) by ;
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 ;
then consider x being object such that
A19: X \ A = {x} by CARD_2:42;
x in X by ;
hence b in X by ; :: thesis: verum
end;
then reconsider f = f as Function of X,X by ;
A20: dom the point-map of F = the Points of (G_ (k,X)) by FUNCT_2:52;
A21: f is one-to-one
proof
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 ;
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 ;
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 ;
f . x1 = union (X \ (F . (c . x1))) by A14;
then f . x1 = y1 by ;
then A1 = A2 by A23, A28, A26, A29, A27, A30, Th5;
then A31: c . x1 = c . x2 by ;
( c . x1 = X \ {x1} & c . x2 = X \ {x2} ) by A4;
then {x1} = {x2} by ;
hence x1 = x2 by ZFMISC_1:3; :: thesis: verum
end;
A32: rng the point-map of F = the Points of (G_ (k,X)) by ;
for y being object st y in X holds
ex x being object st
( x in X & y = f . x )
proof
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 ;
then X \ {y} in rng the point-map of F by ;
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 ;
then consider x being object such that
A37: X \ a = {x} by CARD_2:42;
reconsider x = x as Element of X by ;
a /\ X = X \ {x} by ;
then A38: X \ {x} = a by ;
c . x = X \ {x} by A4;
then X /\ {y} = X \ (F . (c . x)) by ;
then {y} = X \ (F . (c . x)) by ;
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;
then A39: rng f = X by FUNCT_2:10;
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
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 ;
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 ;
then A46: F . A = X \ {(union (X \ (F . A)))} by ;
A47: f .: X = X by ;
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 ;
card (X \ A) = (k + 1) - k by ;
then consider x1 being object such that
A50: X \ A = {x1} by CARD_2:42;
reconsider x1 = x1 as Element of X by ;
A51: ( c . x1 = X \ {x1} & Im (f,x1) = {(f . x1)} ) by ;
(incprojmap (k,f)) . A = f .: A by ;
then (incprojmap (k,f)) . A = (f .: X) \ (f .: {x1}) by ;
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;
dom the point-map of (incprojmap (k,f)) = the Points of (G_ (k,X)) by FUNCT_2:52;
then A52: the point-map of F = the point-map of (incprojmap (k,f)) by ;
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
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 ;
ex A11 being Subset of X st
( x = A11 & card A11 = k + 1 ) by ;
then A58: x = X by ;
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 ; :: thesis: verum
end;
dom the line-map of (incprojmap (k,f)) = the Lines of (G_ (k,X)) by FUNCT_2:52;
then IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,f) by ;
hence ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ; :: thesis: verum