let GS be GraphStruct; :: thesis: for x being set
for n1, n2 being Nat st n1 <> n2 holds
GS . n2 = (GS .set (n1,x)) . n2
let x be set ; :: thesis: for n1, n2 being Nat st n1 <> n2 holds
GS . n2 = (GS .set (n1,x)) . n2
let n1, n2 be Nat; :: thesis: ( n1 <> n2 implies GS . n2 = (GS .set (n1,x)) . n2 )
assume n1 <> n2 ; :: thesis: GS . n2 = (GS .set (n1,x)) . n2
then not n2 in dom (n1 .--> x) by TARSKI:def 1;
hence GS . n2 = (GS .set (n1,x)) . n2 by FUNCT_4:11; :: thesis: verum