theorem Th9: :: WAYBEL27:9

for f being Function
for i, A being set st [:A,{i}:] c= dom f holds
pi (((curry f) .: A),i) = f .: [:A,{i}:]