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

( 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