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 that
A1: [:X,Y:] <> {} and
A2: dom f = [:X,Y:] ; :: thesis: ( dom (curry f) = X & dom (curry' f) = Y )
dom (curry f) = proj1 (dom f) by Def3;
hence dom (curry f) = X by A1, A2, Th11; :: thesis: dom (curry' f) = Y
thus dom (curry' f) = proj1 (dom (~ f)) by Def3
.= proj1 [:Y,X:] by A2, FUNCT_4:47
.= Y by A1, Th11 ; :: thesis: verum