theorem Th32:
for
k being
Nat for
X being non
empty set st
0 < k &
k + 3
c= card X holds
for
F being
IncProjMap over
G_ (
(k + 1),
X),
G_ (
(k + 1),
X) st
F is
automorphism holds
for
H being
IncProjMap over
G_ (
k,
X),
G_ (
k,
X) st the
line-map of
H = the
point-map of
F holds
for
f being
Permutation of
X st
IncProjMap(# the
point-map of
H, the
line-map of
H #)
= incprojmap (
k,
f) holds
IncProjMap(# the
point-map of
F, the
line-map of
F #)
= incprojmap (
(k + 1),
f)