deffunc H_{1}( 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 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_{1}(x)
from FUNCT_1:sch 3();

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

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 A3, A5, FUNCT_2:2;

deffunc H_{2}( 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_{2}(x)
from FUNCT_1:sch 4();

rng f c= X

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

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 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

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

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: verum

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 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

A5: 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

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: verum

end;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 A3, A4, A6, ZFMISC_1:31;

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

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 A3, A5, FUNCT_2:2;

deffunc H

consider f being Function such that

A10: dom f = X and

A11: 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 A10, 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

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: verum

end;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 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: verum

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

A29:
rng the point-map of F = the Points of (G_ (k,X))
by A9, 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

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 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: verum

end;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 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: verum

for y being object st y in X holds

ex x being object st

( x in X & y = f . x )

proof

then
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 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: 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 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: verum

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

A62:
for x being object st x in dom the point-map of F holds
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 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: verum

end;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 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: verum

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 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 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: verum

end;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 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: verum

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: verum