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