let X, Y be set ; :: thesis: for f being Function st [:X,Y:] <> {} & dom f = [:X,Y:] holds
( dom (curry f) = X & dom (curry' f) = Y )
let f be Function; :: thesis: ( [:X,Y:] <> {} & dom f = [:X,Y:] implies ( dom (curry f) = X & dom (curry' f) = Y ) )
assume A1: ( [:X,Y:] <> {} & dom f = [:X,Y:] ) ; :: thesis: ( dom (curry f) = X & dom (curry' f) = Y )
then ( dom (curry f) = proj1 (dom f) & Y <> {} & X <> {} ) by Def3, ZFMISC_1:113;
hence dom (curry f) = X by A1, Th11; :: thesis: dom (curry' f) = Y
thus dom (curry' f) = proj1 (dom (~ f)) by Def3
.= proj1 [:Y,X:] by A1, FUNCT_4:47
.= Y by A1, Th11 ; :: thesis: verum