let X, Y be set ; :: thesis: for f being Function st dom f c= [:X,Y:] holds
( dom (curry f) c= X & dom (curry' f) c= Y )
let f be Function; :: thesis: ( dom f c= [:X,Y:] implies ( dom (curry f) c= X & dom (curry' f) c= Y ) )
assume dom f c= [:X,Y:] ; :: thesis: ( dom (curry f) c= X & dom (curry' f) c= Y )
then A1: ( dom (curry f) = proj1 (dom f) & proj1 (dom f) c= X & dom (~ f) c= [:Y,X:] ) by Def3, Th13, FUNCT_4:46;
hence dom (curry f) c= X ; :: thesis: dom (curry' f) c= Y
dom (curry' f) = proj1 (dom (~ f)) by Def3;
hence dom (curry' f) c= Y by A1, Th13; :: thesis: verum