theorem Th12: :: TOPS_5:12

for x, y, z being object holds (x .--> y) +* (x .--> z) = x .--> z