for D1, D2, D being non empty set
for f being Function of [:D1,D2:],D
for A being set
for f1 being Function of A,D1
for f2 being Function of A,D2
for x being set st x in A holds
((f,D) .: A) .. (f1,f2,x) = f . ((f1 . x),(f2 . x))