reconsider f = _E as the_Edges_of G1 -defined the_Edges_of G2 -valued Function by TARSKI:1;

( dom f c= the_Edges_of G1 & rng f c= the_Edges_of G2 ) ;

hence _E is PartFunc of (the_Edges_of G1),(the_Edges_of G2) by RELSET_1:4; :: thesis: verum

( dom f c= the_Edges_of G1 & rng f c= the_Edges_of G2 ) ;

hence _E is PartFunc of (the_Edges_of G1),(the_Edges_of G2) by RELSET_1:4; :: thesis: verum