let x, y be set ; :: thesis: for f being Function st [x,y] in dom f holds
( x in dom (curry f) & (curry f) . x is Function )
let f be Function; :: thesis: ( [x,y] in dom f implies ( x in dom (curry f) & (curry f) . x is Function ) )
assume [x,y] in dom f ; :: thesis: ( x in dom (curry f) & (curry f) . x is Function )
then A1: x in proj1 (dom f) by RELAT_1:def 4;
hence x in dom (curry f) by Def3; :: thesis: (curry f) . x is Function
ex g being Function st
( (curry f) . x = g & dom g = proj2 ((dom f) /\ [:{x},(proj2 (dom f)):]) & ( for y being set st y in dom g holds
g . y = f . (x,y) ) ) by A1, Def3;
hence (curry f) . x is Function ; :: thesis: verum