theorem :: NDIFF_6:1

for D, E, F being non empty set ex I being Function of (Funcs (D,(Funcs (E,F)))),(Funcs ([:D,E:],F)) st
( I is bijective & ( for f being Function of D,(Funcs (E,F))
for d, e being object st d in D & e in E holds
(I . f) . (d,e) = (f . d) . e ) )