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 Th31; :: thesis: verum