theorem :: FUNCT_5:72

for A, B, C being non empty set
for f being Function of A,(Funcs (B,C))
for a being Element of A
for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b