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