theorem :: FUNCOP_1:18

for h being Function
for A being set
for x being object st A <> {} & x in dom h holds
dom (h * (A --> x)) <> {}