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 A1: dom f c= [:X,Y:] ; :: thesis: ( dom (curry f) c= X & dom (curry' f) c= Y )
dom (curry f) = proj1 (dom f) by Def1;
hence dom (curry f) c= X by A1, Th5; :: thesis: dom (curry' f) c= Y
A2: dom (curry' f) = proj1 (dom (~ f)) by Def1;
dom (~ f) c= [:Y,X:] by A1, FUNCT_4:45;
hence dom (curry' f) c= Y by A2, Th5; :: thesis: verum