f [-] c = f [+] (- c) ;
hence f [-] c is PartFunc of X,(R_PFuncs (DOMS Y)) ; :: thesis: verum