theorem :: TOPREALC:30

for X being set
for c being Complex
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [-] c = f <-> ((dom f) --> c)