theorem Th88: :: FUNCOP_1:88

for x, y being set holds rng (x .--> y) = {y}