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

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

( F is automorphism iff 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: ( 0 < k & k + 1 c= card X implies for F being IncProjMap over G_ (k,X), G_ (k,X) holds

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

assume that

A1: 0 < k and

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

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

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

A3: ( 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) )

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

( F is automorphism iff 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: ( 0 < k & k + 1 c= card X implies for F being IncProjMap over G_ (k,X), G_ (k,X) holds

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

assume that

A1: 0 < k and

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

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

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

A3: ( 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) )

proof

( ex s being Permutation of X st IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) implies F is automorphism )
A4:
( card k = k & succ 1 = 1 + 1 )
;

A5: card (k + 1) = k + 1 ;

k + 1 in succ (card X) by A2, ORDINAL1:22;

then A6: ( k + 1 = card X or k + 1 in card X ) by ORDINAL1:8;

A7: card 1 = 1 ;

( 0 + 1 < k + 1 & succ (Segm k) = Segm (k + 1) ) by A1, NAT_1:38, XREAL_1:8;

then Segm 1 in succ (Segm k) by A7, A5, NAT_1:41;

then ( 1 = k or Segm 1 in Segm k ) by ORDINAL1:8;

then A8: ( 1 = k or ( 1 < k & Segm 2 c= Segm k ) ) by A7, A4, NAT_1:41, ORDINAL1:21;

assume A9: 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)

succ (Segm (k + 1)) = Segm ((k + 1) + 1) by NAT_1:38;

then ( 1 = k or ( 1 < k & card X = k + 1 ) or ( 2 <= k & k + 2 c= card X ) ) by A6, A8, NAT_1:39, ORDINAL1:21;

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

end;A5: card (k + 1) = k + 1 ;

k + 1 in succ (card X) by A2, ORDINAL1:22;

then A6: ( k + 1 = card X or k + 1 in card X ) by ORDINAL1:8;

A7: card 1 = 1 ;

( 0 + 1 < k + 1 & succ (Segm k) = Segm (k + 1) ) by A1, NAT_1:38, XREAL_1:8;

then Segm 1 in succ (Segm k) by A7, A5, NAT_1:41;

then ( 1 = k or Segm 1 in Segm k ) by ORDINAL1:8;

then A8: ( 1 = k or ( 1 < k & Segm 2 c= Segm k ) ) by A7, A4, NAT_1:41, ORDINAL1:21;

assume A9: 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)

succ (Segm (k + 1)) = Segm ((k + 1) + 1) by NAT_1:38;

then ( 1 = k or ( 1 < k & card X = k + 1 ) or ( 2 <= k & k + 2 c= card X ) ) by A6, A8, NAT_1:39, ORDINAL1:21;

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

proof

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

then consider s being Permutation of X such that

A10: IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ;

A11: incprojmap (k,s) is automorphism by A1, A2, Th34;

then A12: incprojmap (k,s) is incidence_preserving ;

A13: F is incidence_preserving

hence F is automorphism by A13; :: thesis: verum

end;then consider s being Permutation of X such that

A10: IncProjMap(# the point-map of F, the line-map of F #) = incprojmap (k,s) ;

A11: incprojmap (k,s) is automorphism by A1, A2, Th34;

then A12: incprojmap (k,s) is incidence_preserving ;

A13: F is incidence_preserving

proof

( the line-map of F is bijective & the point-map of F is bijective )
by A10, A11;
let A be POINT of (G_ (k,X)); :: according to COMBGRAS:def 8 :: thesis: for L1 being LINE of (G_ (k,X)) holds

( A on L1 iff F . A on F . L1 )

let L be LINE of (G_ (k,X)); :: thesis: ( A on L iff F . A on F . L )

( F . A = (incprojmap (k,s)) . A & F . L = (incprojmap (k,s)) . L ) by A10;

hence ( A on L iff F . A on F . L ) by A12; :: thesis: verum

end;( A on L1 iff F . A on F . L1 )

let L be LINE of (G_ (k,X)); :: thesis: ( A on L iff F . A on F . L )

( F . A = (incprojmap (k,s)) . A & F . L = (incprojmap (k,s)) . L ) by A10;

hence ( A on L iff F . A on F . L ) by A12; :: thesis: verum

hence F is automorphism by A13; :: thesis: verum