theorem :: MARGREL1:19

for A being non empty set
for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A)