I'm assuming you want to achieve this in the set.mm database for set theory with classical logic. In that case, everything is a set (or a class), and therefore we have to look for sets which can represent your points.
I see at least three ways to do that:
Using ordered pairs
This is probably the most simple and natural way. In this case abscissa would be the first component of the pair, which can be extracted with 1st, and ordinate would be the second component of the pair, which can be extracted with 2nd.
Your points would then be elements of the cartesian product of the set of the real numbers, RR, with itself: ( RR X. RR )
Given X and Y, one would build a point by constructing an ordered pair, noted as <. X , Y >..
Your theorem would then be written something like:
|- ( P e. ( RR X. RR ) -> <. ( 1st ` P ) , ( 2nd ` P ) .> = P )
This is a special case of the theorem 1st2nd2 which is already in the set.mm database.
Using complex numbers
These are naturally well suited for representing points on the plane, so you will be able to apply e.g. translations/rotations. In this case you extract the abscissa by using the Re function, which gives the real part of the complex number, and the ordinate using the Im function, which gives the imaginary part.
Your points will be elements of the complex number, noted CC.
Given X and Y, to build back the corresponding complex number, one multiplies the imaginary part with the imaginary unit _i and add the real part, so ( X + ( _i x. Y ) ).
So your theorem will then be stated as:
|- ( P e. CC -> P = ( ( Re ` P ) + ( _i x. ( Im ` P ) ) ) )
This is the theorem replim which is already in the set.mm database.
Using a function
This is nearer the usual concept of (computer science) class, and the notation you've used.
In this case the points will be functions, with for example the abscissa being the function evaluated at 0, ( P ` 0 ), and the ordinate being the function evaluated at 1, ( P ` 1 ). Note that instead of 0 and 1, any two values could have been used, those are just possible choices as an example.
In this case your points will be function from the unordered pair { 0 , 1 } into the real numbers RR. This set can be written using the power notation: ( RR ^m { 0 , 1 } ). We could also have used the notation P : { 0 , 1 } --> RR.
Behind the scenes, functions are collections of ordered pairs, so in order to build back "point object" from X and Y, its values at 0 and 1, you will build a set containing those two function evaluations.
This is written { <. 0 , X >. , <. 1 , Y >. }.
Your theorem will look like this:
|- ( P e. ( RR ^m { 0 , 1 } ) -> F = { <. 0 , ( P ` 0 ) >. , <. 1 , ( P ` 1 ) >. } )
This formulation is not directly in the database, but could easily be derived from e.g. fnpr2g
This last option would be similar to the way points of the Euclidean vector space / Hilbert space of two dimensions is encoded in set.mm, see ehlbase for N = 2.
