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