let F be PGraphMapping of G1,G2; :: thesis: F is one-to-one
( dom (F _V) is trivial & dom (F _E) is trivial ) by ZFMISC_1:130;
then ( F _V is trivial & F _E is trivial ) ;
hence F is one-to-one ; :: thesis: verum