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 )
set G2 = GS .set n1,x;
A1: dom (n1 .--> x) = {n1} by FUNCOP_1:19;
assume n1 <> n2 ; :: thesis: GS . n2 = (GS .set n1,x) . n2
then not n2 in dom (n1 .--> x) by A1, TARSKI:def 1;
hence GS . n2 = (GS .set n1,x) . n2 by FUNCT_4:12; :: thesis: verum