let x, y be set ; :: thesis: for f, g being Function st [x,y] in dom f & g = (curry' f) . y holds
( x in dom g & g . x = f . (x,y) )
let f, g be Function; :: thesis: ( [x,y] in dom f & g = (curry' f) . y implies ( x in dom g & g . x = f . (x,y) ) )
assume [x,y] in dom f ; :: thesis: ( not g = (curry' f) . y or ( x in dom g & g . x = f . (x,y) ) )
then A1: [y,x] in dom (~ f) by FUNCT_4:43;
assume A2: g = (curry' f) . y ; :: thesis: ( x in dom g & g . x = f . (x,y) )
then g . x = (~ f) . (y,x) by A1, Th27;
hence ( x in dom g & g . x = f . (x,y) ) by A1, A2, Th27, FUNCT_4:44; :: thesis: verum