for S, T being non empty 1-sorted
for s being Point of S
for t being Point of T holds (S --> t) . s = t ;