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) . c) . d
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) . c) . d
let d be Element of D; :: thesis: for f being Function of [:C,D:],E holds f . (c,d) = ((curry f) . c) . d
let f be Function of [:C,D:],E; :: thesis: f . (c,d) = ((curry f) . c) . d
[c,d] in [:C,D:] ;
then [c,d] in dom f by FUNCT_2:def 1;
hence f . (c,d) = ((curry f) . c) . d by Th13; :: thesis: verum