let A, B, C be 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
let f be 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
let a be Element of A; for b being Element of B holds (uncurry f) . (a,b) = (f . a) . b
let b be Element of B; (uncurry f) . (a,b) = (f . a) . b
( dom f = A & dom (f . a) = B )
by FUNCT_2:def 1;
hence
(uncurry f) . (a,b) = (f . a) . b
by FUNCT_5:38; verum