set IT = G +* (n .--> x);
A1: dom (G +* (n .--> x)) = (dom G) \/ (dom (n .--> x)) by FUNCT_4:def 1;
A2: dom G c= NAT by RELAT_1:def 18;
n in NAT by ORDINAL1:def 13;
then A3: {n} c= NAT by ZFMISC_1:37;
dom (n .--> x) = {n} by FUNCOP_1:19;
then dom (G +* (n .--> x)) c= NAT by A1, A2, A3, XBOOLE_1:8;
hence G +* (n .--> x) is GraphStruct by RELAT_1:def 18; :: thesis: verum