let GS be GraphStruct; :: thesis: for x being set
for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n}
let x be set ; :: thesis: for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n}
let n be Nat; :: thesis: dom (GS .set (n,x)) = (dom GS) \/ {n}
set G2 = GS .set (n,x);
thus dom (GS .set (n,x)) = (dom GS) \/ (dom (n .--> x)) by FUNCT_4:def 1
.= (dom GS) \/ {n} ; :: thesis: verum