let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
for F being IncProjMap of 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 of 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 of 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 of 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

A4: ( card k = k & succ 1 = 1 + 1 ) by CARD_1:def 5;
A5: card (k + 1) = k + 1 by CARD_1:def 5;
k + 1 in succ (card X) by A2, ORDINAL1:34;
then A6: ( k + 1 = card X or k + 1 in card X ) by ORDINAL1:13;
A7: card 1 = 1 by CARD_1:def 5;
( 0 + 1 < k + 1 & succ k = k + 1 ) by A1, NAT_1:39, XREAL_1:10;
then 1 in succ k by A7, A5, NAT_1:42;
then ( 1 = k or 1 in k ) by ORDINAL1:13;
then A8: ( 1 = k or ( 1 < k & 2 c= k ) ) by A7, A4, NAT_1:42, ORDINAL1:33;
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 (k + 1) = (k + 1) + 1 by NAT_1:39;
then ( 1 = k or ( 1 < k & card X = k + 1 ) or ( 2 <= k & k + 2 c= card X ) ) by A6, A8, NAT_1:40, ORDINAL1:33;
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;

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

proof

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 by Def9;
A13: F is incidence_preserving

proof

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, Def8; :: thesis: verum

end;

( the line-map of F is bijective & the point-map of F is bijective ) by A10, A11, Def9;
hence F is automorphism by A13, Def9; :: thesis: verum

end;

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