theorem LM5: :: LOPBAN_8:8

for E, F, G being non empty set
for f being Function of [:E,F:],G
for x, y being object st x in E & y in F holds
((curry' f) . y) . x = f . (x,y)