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