let C, D, E be non empty set ; 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; 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; for f being Function of [:C,D:],E holds f . (c,d) = ((curry' f) . d) . c
let f be Function of [:C,D:],E; 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; verum