theorem :: FUNCOP_1:15

for A being set
for x being object holds (A --> x) " {x} = A