deffunc H1( set ) -> set = s .: $1;
consider P being Function such that
A2:
( dom P = the Points of (G_ (k,X)) & ( for x being set st x in the Points of (G_ (k,X)) holds
P . x = H1(x) ) )
from FUNCT_1:sch 5();
A3:
the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k }
by A1, Def1;
rng P c= the Points of (G_ (k,X))
proof
let b be
object ;
TARSKI:def 3 ( not b in rng P or b in the Points of (G_ (k,X)) )
reconsider bb =
b as
set by TARSKI:1;
assume
b in rng P
;
b in the Points of (G_ (k,X))
then consider a being
object such that A4:
a in the
Points of
(G_ (k,X))
and A5:
b = P . a
by A2, FUNCT_1:def 3;
consider A being
Subset of
X such that A6:
A = a
and A7:
card A = k
by A3, A4;
A8:
b = s .: A
by A2, A4, A5, A6;
A9:
bb c= X
dom s = X
by FUNCT_2:def 1;
then
card bb = k
by A7, A8, Th4;
hence
b in the
Points of
(G_ (k,X))
by A3, A9;
verum
end;
then reconsider P = P as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A2, FUNCT_2:2;
A10:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A1, Def1;
consider L being Function such that
A11:
( dom L = the Lines of (G_ (k,X)) & ( for x being set st x in the Lines of (G_ (k,X)) holds
L . x = H1(x) ) )
from FUNCT_1:sch 5();
rng L c= the Lines of (G_ (k,X))
proof
let b be
object ;
TARSKI:def 3 ( not b in rng L or b in the Lines of (G_ (k,X)) )
reconsider bb =
b as
set by TARSKI:1;
assume
b in rng L
;
b in the Lines of (G_ (k,X))
then consider a being
object such that A12:
a in the
Lines of
(G_ (k,X))
and A13:
b = L . a
by A11, FUNCT_1:def 3;
consider A being
Subset of
X such that A14:
A = a
and A15:
card A = k + 1
by A10, A12;
A16:
b = s .: A
by A11, A12, A13, A14;
A17:
bb c= X
dom s = X
by FUNCT_2:def 1;
then
card bb = k + 1
by A15, A16, Th4;
hence
b in the
Lines of
(G_ (k,X))
by A10, A17;
verum
end;
then reconsider L = L as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by A11, FUNCT_2:2;
take
IncProjMap(# P,L #)
; ( ( for A being POINT of (G_ (k,X)) holds IncProjMap(# P,L #) . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds IncProjMap(# P,L #) . L = s .: L ) )
thus
( ( for A being POINT of (G_ (k,X)) holds IncProjMap(# P,L #) . A = s .: A ) & ( for L being LINE of (G_ (k,X)) holds IncProjMap(# P,L #) . L = s .: L ) )
by A2, A11; verum