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 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,Glet e,
v,
w be
object ;
( 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)) )
;
( 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
;
(id (the_Edges_of G)) . e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,Gthen
(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;
verum end;
hence
[(id (the_Vertices_of G)),(id (the_Edges_of G))] is PGraphMapping of G,G
by A1, Th8; verum