Constraint for Total Functions Follow

Hello,

I have a DSL for Total Functions, like : TotalFunction f = X -> Y { < x1 > |-> < y1 > }
< x2 > |-> < y2 >
< x3 > |-> < y3 >  

The Elements in the Function is defined as finite Sets, like: FinSet X = { x1 x2 x3 };
FinSet Y = { y1 y2 y3 }; 

At the moment all FinSet-Elements can be chosen, that means on the left side you can choose all Elements of X and Y, but

in this case on the left side, only Elements of FinSet X shall be allowed, for the right side it should be the same with only Elements of Y. 

Now, I had the idea to do a constraint for "Mapping" and do a referent constraint for "from" and "to". In this case I had tried something for "from" first of all, but It doesn't work at all and I have absolutely no idea, how to handle this. Please help:

The pictures below show, how the language looks exactly:

Thank you in advance.

Best regards,

Volker