theorem :: FUNCOP_1:89

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