set IT = [(id (the_Vertices_of G)),(id (the_Edges_of G))];
A1: for e being object st e in dom (id (the_Edges_of G)) holds
( (the_Source_of G) . e in dom (id (the_Vertices_of G)) & (the_Target_of G) . e in dom (id (the_Vertices_of G)) ) by FUNCT_2:5;

now :: thesis: for e, v, w being object st e in dom (id (the_Edges_of G)) & v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins v,w,G holds
(id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G

let e, v, w be object ; :: thesis: ( e in dom (id (the_Edges_of G)) & v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins v,w,G implies (id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G )
assume A2: ( e in dom (id (the_Edges_of G)) & v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) ) ; :: thesis: ( e Joins v,w,G implies (id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G )
assume e Joins v,w,G ; :: thesis: (id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G
then (id (the_Edges_of G)) . e Joins v,w,G by A2, FUNCT_1:18;
then (id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,w,G by A2, FUNCT_1:18;
hence (id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G by A2, FUNCT_1:18; :: thesis: verum

end;

hence [(id (the_Vertices_of G)),(id (the_Edges_of G))] is PGraphMapping of G,G by A1, Th8; :: thesis: verum