let f, g be Function; :: thesis: for x, y being object st [x,y] in dom f & g = (curry' f) . y holds
( x in dom g & g . x = f . (x,y) )
let x, y be object ; :: 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:42;
assume A2: g = (curry' f) . y ; :: thesis: ( x in dom g & g . x = f . (x,y) )
then g . x = (~ f) . (y,x) by A1, Th13;
hence ( x in dom g & g . x = f . (x,y) ) by A1, A2, Th13, FUNCT_4:43; :: thesis: verum