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