let z, x, y be set ; :: thesis: dom ((x --> y) +* (x .--> z)) = succ x
thus dom ((x --> y) +* (x .--> z)) = (dom (x --> y)) \/ (dom (x .--> z)) by Def1
.= x \/ (dom (x .--> z)) by FUNCOP_1:19
.= x \/ {x} by FUNCOP_1:19
.= succ x by ORDINAL1:def 1 ; :: thesis: verum