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} by FUNCOP_1:19 ; :: thesis: verum