theorem Th3: :: BOOLMARK:3

for A, B being set
for f being Function
for x being set st A misses B holds
(f +* (A --> x)) .: B = f .: B