let G1, G2 be _Graph; :: thesis: [{},{}] is PGraphMapping of G1,G2

consider f, g being Function such that

A1: [{},{}] = [f,g] and

A2: ( 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 ) and

A3: 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 ) and

for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) and

A4: 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 by Lm2;

thus [{},{}] is PGraphMapping of G1,G2 by A1, A2, A3, A4, Def8; :: thesis: verum

consider f, g being Function such that

A1: [{},{}] = [f,g] and

A2: ( 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 ) and

A3: 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 ) and

for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) and

A4: 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 by Lm2;

thus [{},{}] is PGraphMapping of G1,G2 by A1, A2, A3, A4, Def8; :: thesis: verum