deffunc H1( object ) -> set = {\$1};
let k be Nat; :: thesis: for X being non empty set st k = 1 & k + 1 c= card X 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: ( k = 1 & k + 1 c= card X 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 A1: ( k = 1 & k + 1 c= 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)

A2: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = 1 } by ;
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: 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
A6: ( x in dom c & y = c . x ) by FUNCT_1:def 3;
A7: card {x} = 1 by CARD_1:30;
( {x} c= X & y = {x} ) by ;
hence y in the Points of (G_ (k,X)) by A2, A7; :: 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 A8: 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)
A9: the point-map of F is bijective by A8;
reconsider c = c as Function of X, the Points of (G_ (k,X)) by ;
deffunc H2( Element of X) -> set = union (F . (c . \$1));
consider f being Function such that
A10: dom f = X and
A11: 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
A12: a in X and
A13: b = f . a by ;
reconsider a = a as Element of X by A12;
A14: b = union (F . (c . a)) by ;
consider A being POINT of (G_ (k,X)) such that
A15: A = F . (c . a) ;
A in the Points of (G_ (k,X)) ;
then A16: ex A1 being Subset of X st
( A1 = A & card A1 = 1 ) by A2;
then consider x being object such that
A17: 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 ;
A18: F is incidence_preserving by A8;
A19: dom the point-map of F = the Points of (G_ (k,X)) by FUNCT_2:52;
A20: 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
A21: ( x1 in dom f & x2 in dom f ) and
A22: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of X by A21;
consider A1 being POINT of (G_ (k,X)) such that
A23: A1 = F . (c . x1) ;
A1 in the Points of (G_ (k,X)) ;
then ex A11 being Subset of X st
( A11 = A1 & card A11 = 1 ) by A2;
then consider y1 being object such that
A24: A1 = {y1} by CARD_2:42;
A25: ( c . x1 = {x1} & c . x2 = {x2} ) by A4;
consider A2 being POINT of (G_ (k,X)) such that
A26: A2 = F . (c . x2) ;
A2 in the Points of (G_ (k,X)) ;
then ex A12 being Subset of X st
( A12 = A2 & card A12 = 1 ) by A2;
then consider y2 being object such that
A27: A2 = {y2} by CARD_2:42;
f . x2 = union (F . (c . x2)) by A11;
then A28: f . x2 = y2 by ;
f . x1 = union (F . (c . x1)) by A11;
then f . x1 = y1 by ;
then c . x1 = c . x2 by ;
hence x1 = x2 by ; :: thesis: verum
end;
A29: 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 A30: {y} c= X by ZFMISC_1:31;
card {y} = 1 by CARD_1:30;
then {y} in rng the point-map of F by A2, A29, A30;
then consider a being object such that
A31: a in dom the point-map of F and
A32: {y} = the point-map of F . a by FUNCT_1:def 3;
a in the Points of (G_ (k,X)) by A31;
then A33: ex A1 being Subset of X st
( A1 = a & card A1 = 1 ) by A2;
then consider x being object such that
A34: a = {x} by CARD_2:42;
reconsider x = x as Element of X by ;
{y} = F . (c . x) by A4, A32, A34;
then y = union (F . (c . x)) by ZFMISC_1:25;
then y = f . x by A11;
hence ex x being object st
( x in X & y = f . x ) ; :: thesis: verum
end;
then 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 A20;
A35: dom the line-map of F = the Lines of (G_ (k,X)) by FUNCT_2:52;
A36: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = 1 + 1 } by ;
A37: 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 A38: 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
A39: x = A ;
consider A11 being Subset of X such that
A40: x = A11 and
A41: card A11 = 2 by ;
consider x1, x2 being object such that
A42: x1 <> x2 and
A43: x = {x1,x2} by ;
reconsider x1 = x1, x2 = x2 as Element of X by ;
c . x1 = {x1} by A4;
then consider A1 being POINT of (G_ (k,X)) such that
A44: A1 = {x1} ;
c . x2 = {x2} by A4;
then consider A2 being POINT of (G_ (k,X)) such that
A45: A2 = {x2} ;
A1 <> A2 by ;
then A46: F . A1 <> F . A2 by ;
F . A2 in the Points of (G_ (k,X)) ;
then A47: ex B2 being Subset of X st
( B2 = F . A2 & card B2 = 1 ) by A2;
then consider y2 being object such that
A48: F . A2 = {y2} by CARD_2:42;
A1 c= A by ;
then A1 on A by ;
then F . A1 on F . A by A18;
then A49: F . A1 c= F . A by ;
A50: ( (incprojmap (k,f)) . A = f .: A & f .: (A1 \/ A2) = (f .: A1) \/ (f .: A2) ) by ;
A51: A1 \/ A2 = A by ;
F . A1 in the Points of (G_ (k,X)) ;
then A52: ex B1 being Subset of X st
( B1 = F . A1 & card B1 = 1 ) by A2;
then A53: ex y1 being object st F . A1 = {y1} by CARD_2:42;
A2 c= A by ;
then A2 on A by ;
then F . A2 on F . A by A18;
then A54: F . A2 c= F . A by ;
F . (c . x2) = F . A2 by ;
then A55: f . x2 = union (F . A2) by A11;
Im (f,x2) = {(f . x2)} by ;
then A56: f .: A2 = F . A2 by ;
A57: F . A1 is finite by A52;
not y2 in F . A1 by ;
then A58: card ((F . A1) \/ (F . A2)) = 1 + 1 by ;
F . (c . x1) = F . A1 by ;
then A59: f . x1 = union (F . A1) by A11;
Im (f,x1) = {(f . x1)} by ;
then A60: f .: A1 = F . A1 by ;
F . A in the Lines of (G_ (k,X)) ;
then A61: ex B3 being Subset of X st
( B3 = F . A & card B3 = 2 ) by A36;
then F . A is finite ;
hence the line-map of F . x = the line-map of (incprojmap (k,f)) . x by ; :: thesis: verum
end;
A62: 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 A63: 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
A64: x = A ;
A65: ex A1 being Subset of X st
( x = A1 & card A1 = 1 ) by A2, A19, A63;
then consider x1 being object such that
A66: x = {x1} by CARD_2:42;
reconsider x1 = x1 as Element of X by ;
F . (c . x1) = F . A by A4, A64, A66;
then A67: f . x1 = union (F . A) by A11;
F . A in the Points of (G_ (k,X)) ;
then consider B being Subset of X such that
A68: B = F . A and
A69: card B = 1 by A2;
A70: ex x2 being object st B = {x2} by ;
( (incprojmap (k,f)) . A = f .: A & Im (f,x1) = {(f . x1)} ) by ;
hence the point-map of F . x = the point-map of (incprojmap (k,f)) . x by ; :: thesis: verum
end;
dom the point-map of (incprojmap (k,f)) = the Points of (G_ (k,X)) by FUNCT_2:52;
then A71: the point-map of F = the point-map of (incprojmap (k,f)) by ;
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