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