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;

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

hence
[(id (the_Vertices_of G)),(id (the_Edges_of G))] is PGraphMapping of G,G
by A1, Th8; :: thesis: verum(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;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