dom (f +* (x,y)) = dom f by FUNCT_7:30
.= X by PARTFUN1:def 2 ;
hence for b₁ being X -defined Function st b₁ = f +* (x,y) holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum