theorem Th13: :: FUNCOP_1:13

for A being set
for x being object holds
( dom (A --> x) = A & rng (A --> x) c= {x} )