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