theorem :: VALUED_2:55

for X being set
for Y being complex-functions-membered set
for c being Complex
for f being PartFunc of X,Y holds dom (f [/] c) = dom f by Def39;