let A, B, C be non empty set ; :: thesis: 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); :: thesis: 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; :: thesis: for b being Element of B holds (uncurry f) . a,b = (f . a) . b
let b be Element of B; :: thesis: (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:45; :: thesis: verum