for A being non empty 1-sorted
for B being 1 -element 1-sorted
for t being Point of B
for f being Function of A,B holds f = A --> t