deffunc H₁( object ) -> set = {$1};
let k be Nat; :: thesis:
let X be non empty set ; :: thesis:
assume A1: ( k = 1 & k + 1 c= card X ) ; :: thesis:
A2: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = 1 } by A1, Def1;
consider c being Function such that
A3: dom c = X and
A4: for x being object st x in X holds
c . x = H₁(x) from FUNCT_1:sch 3();
A5: rng c c= the Points of (G_ (k,X))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng c ; :: thesis:
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 A3, A4, A6, ZFMISC_1:31;
hence y in the Points of (G_ (k,X)) by A2, A7; :: thesis:

end;

let F be IncProjMap over G_ (k,X), G_ (k,X); :: thesis:
assume A8: F is automorphism ; :: thesis:
A9: the point-map of F is bijective by A8;
reconsider c = c as Function of X, the Points of (G_ (k,X)) by A3, A5, FUNCT_2:2;
deffunc H₂( 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 = H₂(x) from FUNCT_1:sch 4();
rng f c= X

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng f ; :: thesis:
then consider a being object such that
A12: a in X and
A13: b = f . a by A10, FUNCT_1:def 3;
reconsider a = a as Element of X by A12;
A14: b = union (F . (c . a)) by A11, A13;
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 A16, A17, ZFMISC_1:31;
hence b in X by A14, A15, A17, ZFMISC_1:25; :: thesis:

end;

then reconsider f = f as Function of X,X by A10, FUNCT_2:2;
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:
assume that
A21: ( x1 in dom f & x2 in dom f ) and
A22: f . x1 = f . x2 ; :: thesis:
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 A26, A27, ZFMISC_1:25;
f . x1 = union (F . (c . x1)) by A11;
then f . x1 = y1 by A23, A24, ZFMISC_1:25;
then c . x1 = c . x2 by A9, A19, A22, A23, A26, A24, A27, A28, FUNCT_1:def 4;
hence x1 = x2 by A25, ZFMISC_1:3; :: thesis:

end;

A29: rng the point-map of F = the Points of (G_ (k,X)) by A9, FUNCT_2:def 3;
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:
assume y in X ; :: thesis:
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 A33, A34, ZFMISC_1:31;
{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:

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 A1, Def1;
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:
assume A38: x in dom the line-map of F ; :: thesis:
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 A36, A35, A38;
consider x1, x2 being object such that
A42: x1 <> x2 and
A43: x = {x1,x2} by A40, A41, CARD_2:60;
reconsider x1 = x1, x2 = x2 as Element of X by A40, A43, ZFMISC_1:32;
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 A42, A44, A45, ZFMISC_1:18;
then A46: F . A1 <> F . A2 by A9, A19, FUNCT_1:def 4;
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 A39, A43, A44, ZFMISC_1:36;
then A1 on A by A1, Th10;
then F . A1 on F . A by A18;
then A49: F . A1 c= F . A by A1, Th10;
A50: ( (incprojmap (k,f)) . A = f .: A & f .: (A1 \/ A2) = (f .: A1) \/ (f .: A2) ) by A1, Def14, RELAT_1:120;
A51: A1 \/ A2 = A by A39, A43, A44, A45, ENUMSET1:1;
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 A39, A43, A45, ZFMISC_1:36;
then A2 on A by A1, Th10;
then F . A2 on F . A by A18;
then A54: F . A2 c= F . A by A1, Th10;
F . (c . x2) = F . A2 by A4, A45;
then A55: f . x2 = union (F . A2) by A11;
Im (f,x2) = {(f . x2)} by A10, FUNCT_1:59;
then A56: f .: A2 = F . A2 by A45, A55, A48, ZFMISC_1:25;
A57: F . A1 is finite by A52;
not y2 in F . A1 by A46, A52, A47, A57, A48, CARD_2:102, ZFMISC_1:31;
then A58: card ((F . A1) \/ (F . A2)) = 1 + 1 by A52, A53, A48, CARD_2:41;
F . (c . x1) = F . A1 by A4, A44;
then A59: f . x1 = union (F . A1) by A11;
Im (f,x1) = {(f . x1)} by A10, FUNCT_1:59;
then A60: f .: A1 = F . A1 by A44, A59, A53, ZFMISC_1:25;
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 A39, A50, A51, A49, A54, A61, A58, A60, A56, CARD_2:102, XBOOLE_1:8; :: thesis:

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:
assume A63: x in dom the point-map of F ; :: thesis:
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 A65, A66, ZFMISC_1:31;
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 A69, CARD_2:42;
( (incprojmap (k,f)) . A = f .: A & Im (f,x1) = {(f . x1)} ) by A1, A10, Def14, FUNCT_1:59;
hence the point-map of F . x = the point-map of (incprojmap (k,f)) . x by A64, A66, A67, A68, A70, ZFMISC_1:25; :: thesis:

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 A19, A62;
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 A35, A71, A37, 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: