let k be Element of NAT ; for X being non empty set st 2 <= k & k + 2 c= card X holds
for F being IncProjMap of 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 ; ( 2 <= k & k + 2 c= card X implies for F being IncProjMap of 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 that
A1:
2 <= k
and
A2:
k + 2 c= card X
; for F being IncProjMap of 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
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= k implies for F being IncProjMap of G_ $1,X, G_ $1,X st F is automorphism holds
ex f being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap $1,f );
A3:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )
assume A4:
S1[
i]
;
S1[i + 1]
( 1
<= i + 1 &
i + 1
<= k implies for
F being
IncProjMap of
G_ (i + 1),
X,
G_ (i + 1),
X st
F is
automorphism holds
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F,the
line-map of
F #)
= incprojmap (i + 1),
f )
proof
assume that
1
<= i + 1
and A5:
i + 1
<= k
;
for F being IncProjMap of G_ (i + 1),X, G_ (i + 1),X st F is automorphism holds
ex f being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap (i + 1),f
let F2 be
IncProjMap of
G_ (i + 1),
X,
G_ (i + 1),
X;
( F2 is automorphism implies ex f being Permutation of X st IncProjMap(# the point-map of F2,the line-map of F2 #) = incprojmap (i + 1),f )
assume A6:
F2 is
automorphism
;
ex f being Permutation of X st IncProjMap(# the point-map of F2,the line-map of F2 #) = incprojmap (i + 1),f
(i + 1) + 2
<= k + 2
by A5, XREAL_1:9;
then A7:
i + 3
c= k + 2
by NAT_1:40;
then A8:
i + 3
c= card X
by A2, XBOOLE_1:1;
A9:
(
i = 0 implies ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f )
(
0 < i implies ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f )
proof
assume A11:
0 < i
;
ex f being Permutation of X st IncProjMap(# the point-map of F2,the line-map of F2 #) = incprojmap (i + 1),f
then consider F1 being
IncProjMap of
G_ i,
X,
G_ i,
X such that A12:
F1 is
automorphism
and A13:
the
line-map of
F1 = the
point-map of
F2
and
for
A being
POINT of
(G_ i,X) for
B being
finite set st
B = A holds
F1 . A = meet (F2 .: (^^ B,X,(i + 1)))
by A2, A6, A7, Th31, XBOOLE_1:1;
0 + 1
< i + 1
by A11, XREAL_1:10;
then consider f being
Permutation of
X such that A14:
IncProjMap(# the
point-map of
F1,the
line-map of
F1 #)
= incprojmap i,
f
by A4, A5, A12, NAT_1:13;
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f
by A2, A6, A7, A11, A13, A14, Th32, XBOOLE_1:1;
hence
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f
;
verum
end;
hence
ex
f being
Permutation of
X st
IncProjMap(# the
point-map of
F2,the
line-map of
F2 #)
= incprojmap (i + 1),
f
by A9;
verum
end;
hence
S1[
i + 1]
;
verum
end;
A15:
S1[ 0 ]
;
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A15, A3);
then A16:
S1[k]
;
let F be IncProjMap of G_ k,X, G_ k,X; ( 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 )
assume
F is automorphism
; ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
hence
ex s being Permutation of X st IncProjMap(# the point-map of F,the line-map of F #) = incprojmap k,s
by A1, A16, XXREAL_0:2; verum