theorem :: FUNCOP_1:86

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