let C, D, E be non empty set ; :: thesis: for c being Element of C
for d being Element of D
for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c
let c be Element of C; :: thesis: for d being Element of D
for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c
let d be Element of D; :: thesis: for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c
let f be Function of [:C,D:],E; :: thesis: f . (c,d) = ((curry' f) . d) . c
[c,d] in [:C,D:] ;
then [c,d] in dom f by FUNCT_2:def 1;
hence f . (c,d) = ((curry' f) . d) . c by Th15; :: thesis: verum