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