let k be Nat; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
for s being Permutation of X holds incprojmap (k,s) is automorphism

let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for s being Permutation of X holds incprojmap (k,s) is automorphism )
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: for s being Permutation of X holds incprojmap (k,s) is automorphism
let s be Permutation of X; :: thesis: incprojmap (k,s) is automorphism
A2: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by ;
A3: the point-map of (incprojmap (k,s)) is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom the point-map of (incprojmap (k,s)) or not x2 in dom the point-map of (incprojmap (k,s)) or not the point-map of (incprojmap (k,s)) . x1 = the point-map of (incprojmap (k,s)) . x2 or x1 = x2 )
assume that
A4: x1 in dom the point-map of (incprojmap (k,s)) and
A5: x2 in dom the point-map of (incprojmap (k,s)) and
A6: the point-map of (incprojmap (k,s)) . x1 = the point-map of (incprojmap (k,s)) . x2 ; :: thesis: x1 = x2
consider X1 being POINT of (G_ (k,X)) such that
A7: X1 = x1 by A4;
x1 in the Points of (G_ (k,X)) by A4;
then A8: ex X11 being Subset of X st
( X11 = x1 & card X11 = k ) by A2;
consider X2 being POINT of (G_ (k,X)) such that
A9: X2 = x2 by A5;
x2 in the Points of (G_ (k,X)) by A5;
then A10: ex X12 being Subset of X st
( X12 = x2 & card X12 = k ) by A2;
A11: (incprojmap (k,s)) . X2 = s .: X2 by ;
(incprojmap (k,s)) . X1 = s .: X1 by ;
hence x1 = x2 by A6, A7, A9, A8, A10, A11, Th6; :: thesis: verum
end;
for y being object st y in the Points of (G_ (k,X)) holds
ex x being object st
( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x )
proof
let y be object ; :: thesis: ( y in the Points of (G_ (k,X)) implies ex x being object st
( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x ) )

assume y in the Points of (G_ (k,X)) ; :: thesis: ex x being object st
( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x )

then A12: ex B being Subset of X st
( B = y & card B = k ) by A2;
reconsider y = y as set by TARSKI:1;
A13: s " y c= dom s by RELAT_1:132;
then A14: s " y c= X by FUNCT_2:52;
rng s = X by FUNCT_2:def 3;
then A15: s .: (s " y) = y by ;
then card (s " y) = k by ;
then s " y in the Points of (G_ (k,X)) by ;
then consider A being POINT of (G_ (k,X)) such that
A16: A = s " y ;
y = (incprojmap (k,s)) . A by ;
hence ex x being object st
( x in the Points of (G_ (k,X)) & y = the point-map of (incprojmap (k,s)) . x ) ; :: thesis: verum
end;
then rng the point-map of (incprojmap (k,s)) = the Points of (G_ (k,X)) by FUNCT_2:10;
then A17: the point-map of (incprojmap (k,s)) is onto by FUNCT_2:def 3;
A18: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by ;
for y being object st y in the Lines of (G_ (k,X)) holds
ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x )
proof
let y be object ; :: thesis: ( y in the Lines of (G_ (k,X)) implies ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x ) )

assume y in the Lines of (G_ (k,X)) ; :: thesis: ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x )

then A19: ex B being Subset of X st
( B = y & card B = k + 1 ) by A18;
reconsider y = y as set by TARSKI:1;
A20: s " y c= dom s by RELAT_1:132;
then A21: s " y c= X by FUNCT_2:52;
rng s = X by FUNCT_2:def 3;
then A22: s .: (s " y) = y by ;
then card (s " y) = k + 1 by ;
then s " y in the Lines of (G_ (k,X)) by ;
then consider A being LINE of (G_ (k,X)) such that
A23: A = s " y ;
y = (incprojmap (k,s)) . A by ;
hence ex x being object st
( x in the Lines of (G_ (k,X)) & y = the line-map of (incprojmap (k,s)) . x ) ; :: thesis: verum
end;
then rng the line-map of (incprojmap (k,s)) = the Lines of (G_ (k,X)) by FUNCT_2:10;
then A24: the line-map of (incprojmap (k,s)) is onto by FUNCT_2:def 3;
A25: dom s = X by FUNCT_2:52;
A26: incprojmap (k,s) is incidence_preserving
proof
let A1 be POINT of (G_ (k,X)); :: according to COMBGRAS:def 8 :: thesis: for L1 being LINE of (G_ (k,X)) holds
( A1 on L1 iff (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )

let L1 be LINE of (G_ (k,X)); :: thesis: ( A1 on L1 iff (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
A27: ( s .: A1 = (incprojmap (k,s)) . A1 & s .: L1 = (incprojmap (k,s)) . L1 ) by ;
A1 in the Points of (G_ (k,X)) ;
then A28: ex a1 being Subset of X st
( A1 = a1 & card a1 = k ) by A2;
A29: ( (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 implies A1 on L1 )
proof
assume (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 ; :: thesis: A1 on L1
then s .: A1 c= s .: L1 by ;
then A1 c= L1 by ;
hence A1 on L1 by ; :: thesis: verum
end;
( A1 on L1 implies (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 )
proof
assume A1 on L1 ; :: thesis: (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1
then A1 c= L1 by ;
then s .: A1 c= s .: L1 by RELAT_1:123;
hence (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 by ; :: thesis: verum
end;
hence ( A1 on L1 iff (incprojmap (k,s)) . A1 on (incprojmap (k,s)) . L1 ) by A29; :: thesis: verum
end;
the line-map of (incprojmap (k,s)) is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom the line-map of (incprojmap (k,s)) or not x2 in dom the line-map of (incprojmap (k,s)) or not the line-map of (incprojmap (k,s)) . x1 = the line-map of (incprojmap (k,s)) . x2 or x1 = x2 )
assume that
A30: x1 in dom the line-map of (incprojmap (k,s)) and
A31: x2 in dom the line-map of (incprojmap (k,s)) and
A32: the line-map of (incprojmap (k,s)) . x1 = the line-map of (incprojmap (k,s)) . x2 ; :: thesis: x1 = x2
consider X1 being LINE of (G_ (k,X)) such that
A33: X1 = x1 by A30;
x1 in the Lines of (G_ (k,X)) by A30;
then A34: ex X11 being Subset of X st
( X11 = x1 & card X11 = k + 1 ) by A18;
consider X2 being LINE of (G_ (k,X)) such that
A35: X2 = x2 by A31;
x2 in the Lines of (G_ (k,X)) by A31;
then A36: ex X12 being Subset of X st
( X12 = x2 & card X12 = k + 1 ) by A18;
A37: (incprojmap (k,s)) . X2 = s .: X2 by ;
(incprojmap (k,s)) . X1 = s .: X1 by ;
hence x1 = x2 by A32, A33, A35, A34, A36, A37, Th6; :: thesis: verum
end;
hence incprojmap (k,s) is automorphism by A24, A3, A17, A26; :: thesis: verum