set a = curry f;
( dom f = [:X,Y:] & dom (curry f) = proj1 (dom f) ) by FUNCT_5:def 3, PARTFUN1:def 4;
then dom (curry f) = X by FUNCT_5:11;
hence for b₁ being X -defined Function st b₁ = curry f holds
b₁ is total by PARTFUN1:def 4; :: thesis: verum