for D being non empty set
for E being non-empty non empty FinSequence
for F being non empty set ex L being Function of (Funcs (D,(Funcs ((product E),F)))),(Funcs ((product (E ^ <*D*>)),F)) st
( L is bijective & ( for f being Function of D,(Funcs ((product E),F))
for e being FinSequence
for d being object st e in product E & d in D holds
(L . f) . (e ^ <*d*>) = (f . d) . e ) )