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) & curry' f = curry (~ f) ) by FUNCT_4:43;
assume g = (curry' f) . y ; :: thesis: ( x in dom g & g . x = f . x,y )
then ( x in dom g & g . x = (~ f) . y,x ) by A1, Th27;
hence ( x in dom g & g . x = f . x,y ) by A1, FUNCT_4:44; :: thesis: verum