let z, y be object ; :: thesis: for x being set holds dom ((x --> y) +* (x .--> z)) = succ x
let x 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))
.= x \/ {x}
.= succ x by ORDINAL1:def 1 ; :: thesis: verum