let GS be GraphStruct; :: thesis: for x being set
for n being Nat holds (GS .set (n,x)) . n = x
let x be set ; :: thesis: for n being Nat holds (GS .set (n,x)) . n = x
let n be Nat; :: thesis: (GS .set (n,x)) . n = x
set G2 = GS .set (n,x);
n in dom (n .--> x) by TARSKI:def 1;
hence (GS .set (n,x)) . n = (n .--> x) . n by FUNCT_4:13
.= x by FUNCOP_1:72 ;
:: thesis: verum