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