:: deftheorem Def8 defines PGraphMapping GLIB_010:def 8 :
for G1, G2 being _Graph
for b₃ being object holds
( b₃ is PGraphMapping of G1,G2 iff ex f, g being Function st
( b₃ = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds
g . e Joins f . v,f . w,G2 ) ) );