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 A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by ;
rng P c= the Points of (G_ (k,X))
proof
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 ;
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
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 ;
then y in rng s by FUNCT_1:3;
hence y in X by FUNCT_2:def 3; :: thesis: verum
end;
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; :: thesis: verum
end;
then reconsider P = P as Function of the Points of (G_ (k,X)), the Points of (G_ (k,X)) by ;
A10: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by ;
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 rng L c= the Lines of (G_ (k,X))
proof
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 ;
consider A being Subset of X such that
A14: A = a and
A15: card A = k + 1 by ;
A16: b = s .: A by A11, A12, A13, A14;
A17: bb c= X
proof
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 ;
then y in rng s by FUNCT_1:3;
hence y in X by FUNCT_2:def 3; :: thesis: verum
end;
dom s = X by FUNCT_2:def 1;
then card bb = k + 1 by ;
hence b in the Lines of (G_ (k,X)) by ; :: thesis: verum
end;
then reconsider L = L as Function of the Lines of (G_ (k,X)), the Lines of (G_ (k,X)) by ;
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 ; :: thesis: verum