theorem :: FUNCT_4:110

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