:: deftheorem defines [-] VALUED_2:def 38 :
for Y being complex-functions-membered set
for f being b₁ -valued Function
for c being Complex holds f [-] c = f [+] (- c);