deffunc H_{1}( 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 = H_{1}(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))

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 = H_{1}(x) ) )
from FUNCT_1:sch 5();

rng L c= the Lines of (G_ (k,X))

take IncProjMap(# P,L #) ; :: thesis: ( ( 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; :: thesis: verum

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 = H

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

then reconsider P = P as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by A2, FUNCT_2:2;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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

then card bb = k by A7, A8, Th4;

hence b in the Points of (G_ (k,X)) by A3, A9; :: thesis: verum

end;reconsider bb = b as set by TARSKI:1;

assume b in rng P ; :: thesis: 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

proof

dom s = X
by FUNCT_2:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in bb or y in X )

assume y in bb ; :: thesis: y in X

then ex x being object st

( x in dom s & x in A & y = s . x ) by A8, FUNCT_1:def 6;

then y in rng s by FUNCT_1:3;

hence y in X by FUNCT_2:def 3; :: thesis: verum

end;assume y in bb ; :: thesis: y in X

then ex x being object st

( x in dom s & x in A & y = s . x ) by A8, FUNCT_1:def 6;

then y in rng s by FUNCT_1:3;

hence y in X by FUNCT_2:def 3; :: thesis: verum

then card bb = k by A7, A8, Th4;

hence b in the Points of (G_ (k,X)) by A3, A9; :: thesis: verum

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 = H

rng L c= the Lines of (G_ (k,X))

proof

then reconsider L = L as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by A11, FUNCT_2:2;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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

then card bb = k + 1 by A15, A16, Th4;

hence b in the Lines of (G_ (k,X)) by A10, A17; :: thesis: verum

end;reconsider bb = b as set by TARSKI:1;

assume b in rng L ; :: thesis: 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

proof

dom s = X
by FUNCT_2:def 1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in bb or y in X )

assume y in bb ; :: thesis: y in X

then ex x being object st

( x in dom s & x in A & y = s . x ) by A16, FUNCT_1:def 6;

then y in rng s by FUNCT_1:3;

hence y in X by FUNCT_2:def 3; :: thesis: verum

end;assume y in bb ; :: thesis: y in X

then ex x being object st

( x in dom s & x in A & y = s . x ) by A16, FUNCT_1:def 6;

then y in rng s by FUNCT_1:3;

hence y in X by FUNCT_2:def 3; :: thesis: verum

then card bb = k + 1 by A15, A16, Th4;

hence b in the Lines of (G_ (k,X)) by A10, A17; :: thesis: verum

take IncProjMap(# P,L #) ; :: thesis: ( ( 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; :: thesis: verum