set IT = G +* (n .--> x);
A1: dom (n .--> x) = {n} by FUNCOP_1:13;
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, RELAT_1:def 18;
then dom (G +* (n .--> x)) c= NAT by A2, A1, XBOOLE_1:8;
hence G +* (n .--> x) is GraphStruct by RELAT_1:def 18; :: thesis: verum