theorem :: FUNCOP_1:76

for A being set
for x, y being object st not x in A holds
(x .--> y) | A = {}