theorem Th2: :: NDIFF_6:2

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