:: deftheorem defines <-> VALUED_2:def 42 :
for Y being complex-functions-membered set
for f being b₁ -valued Function
for g being complex-valued Function holds f <-> g = f <+> (- g);